Documentation

Mathlib.Algebra.Order.Monoid.NatCast

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 : α) :
a < a + 1
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 : α) :
a < 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.

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.