Documentation

Mathlib.Algebra.Order.Monoid.NatCast

Order of numerals in an AddMonoidWithOne. #

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

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

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

source
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.

source
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.

source
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.

source
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
Equations
  • ⋯ = ⋯
source
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
Equations
  • ⋯ = ⋯
source
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
Equations
  • ⋯ = ⋯
source
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
source
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.

source
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.

source
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.