Order of numerals in an AddMonoidWithOne. #
theorem
lt_add_one
{α : Type u_1}
[One α]
[AddZeroClass α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(a : α)
:
theorem
lt_one_add
{α : Type u_1}
[One α]
[AddZeroClass α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
(a : α)
:
theorem
zero_le_two
{α : Type u_1}
[AddMonoidWithOne α]
[Preorder α]
[ZeroLEOneClass α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 ≤ 2
theorem
zero_le_three
{α : Type u_1}
[AddMonoidWithOne α]
[Preorder α]
[ZeroLEOneClass α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 ≤ 3
theorem
zero_le_four
{α : Type u_1}
[AddMonoidWithOne α]
[Preorder α]
[ZeroLEOneClass α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 ≤ 4
theorem
one_le_two
{α : Type u_1}
[AddMonoidWithOne α]
[LE α]
[ZeroLEOneClass α]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
1 ≤ 2
theorem
one_le_two'
{α : Type u_1}
[AddMonoidWithOne α]
[LE α]
[ZeroLEOneClass α]
[CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
1 ≤ 2
@[simp]
theorem
zero_lt_two
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 2
See zero_lt_two' for a version with the type explicit.
@[simp]
theorem
zero_lt_three
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 3
See zero_lt_three' for a version with the type explicit.
@[simp]
theorem
zero_lt_four
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 4
See zero_lt_four' for a version with the type explicit.
theorem
zero_lt_two'
(α : Type u_1)
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 2
See zero_lt_two for a version with the type implicit.
theorem
zero_lt_three'
(α : Type u_1)
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 3
See zero_lt_three for a version with the type implicit.
theorem
zero_lt_four'
(α : Type u_1)
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 4
See zero_lt_four for a version with the type implicit.
instance
ZeroLEOneClass.neZero.two
(α : Type u_1)
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
NeZero 2
instance
ZeroLEOneClass.neZero.three
(α : Type u_1)
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
NeZero 3
instance
ZeroLEOneClass.neZero.four
(α : Type u_1)
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
NeZero 4
theorem
one_lt_two
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1]
:
1 < 2
theorem
two_pos
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 2
Alias of zero_lt_two.
See zero_lt_two' for a version with the type explicit.
theorem
three_pos
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 3
Alias of zero_lt_three.
See zero_lt_three' for a version with the type explicit.
theorem
four_pos
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1]
:
0 < 4
Alias of zero_lt_four.
See zero_lt_four' for a version with the type explicit.