Documentation

Mathlib.Algebra.Order.Monoid.NatCast

Order of numerals in an AddMonoidWithOne. #

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
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
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
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
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
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
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
@[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.

@[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.

@[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.

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.

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.

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.

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] :
Equations
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] :
Equations
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] :
Equations
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
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.

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.

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.