Documentation

Mathlib.Algebra.Order.Monoid.NatCast

Order of numerals in an AddMonoidWithOne. #

source
ink
theorem lt_add_one {α : Type u_1} [inst : One α] [inst : AddZeroClass α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) :
a < a + 1
source
ink
theorem lt_one_add {α : Type u_1} [inst : One α] [inst : AddZeroClass α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) :
a < 1 + a
source
ink
theorem zero_le_two {α : Type u_1} [inst : AddMonoidWithOne α] [inst : Preorder α] [inst : ZeroLEOneClass α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
0 ≤ 2
source
ink
theorem zero_le_three {α : Type u_1} [inst : AddMonoidWithOne α] [inst : Preorder α] [inst : ZeroLEOneClass α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
0 ≤ 3
source
ink
theorem zero_le_four {α : Type u_1} [inst : AddMonoidWithOne α] [inst : Preorder α] [inst : ZeroLEOneClass α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
0 ≤ 4
source
ink
theorem one_le_two {α : Type u_1} [inst : AddMonoidWithOne α] [inst : LE α] [inst : ZeroLEOneClass α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
1 ≤ 2
source
ink
theorem one_le_two' {α : Type u_1} [inst : AddMonoidWithOne α] [inst : LE α] [inst : ZeroLEOneClass α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
1 ≤ 2
source
ink
@[simp]
theorem zero_lt_two {α : Type u_1} [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : 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.

source
ink
@[simp]
theorem zero_lt_three {α : Type u_1} [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : 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.

source
ink
@[simp]
theorem zero_lt_four {α : Type u_1} [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : 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.

source
ink
theorem zero_lt_two' (α : Type u_1) [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : 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.

source
ink
theorem zero_lt_three' (α : Type u_1) [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : 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.

source
ink
theorem zero_lt_four' (α : Type u_1) [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : 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.

source
ink
instance ZeroLEOneClass.neZero.two (α : Type u_1) [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
NeZero 2
Equations
source
ink
instance ZeroLEOneClass.neZero.three (α : Type u_1) [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
NeZero 3
Equations
source
ink
instance ZeroLEOneClass.neZero.four (α : Type u_1) [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
NeZero 4
Equations
source
ink
theorem one_lt_two {α : Type u_1} [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
1 < 2
source
ink
theorem two_pos {α : Type u_1} [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
0 < 2

Alias of zero_lt_two.

source
ink
theorem three_pos {α : Type u_1} [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
0 < 3

Alias of zero_lt_three.

source
ink
theorem four_pos {α : Type u_1} [inst : AddMonoidWithOne α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :
0 < 4

Alias of zero_lt_four.