Documentation

Foundation.FirstOrder.Arith.PeanoMinus

Equations
theorem LO.Arith.le_def {M : Type u_1} [ORingStruc M] {x y : M} :
x y x = y x < y
theorem LO.Arith.add_zero {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
x + 0 = x
theorem LO.Arith.add_assoc {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) :
x + y + z = x + (y + z)
theorem LO.Arith.add_comm {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) :
x + y = y + x
theorem LO.Arith.add_eq_of_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) :
x < y∃ (z : M), x + z = y
@[simp]
theorem LO.Arith.zero_le {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
0 x
theorem LO.Arith.one_le_of_zero_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
0 < x1 x
theorem LO.Arith.add_lt_add {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) :
x < yx + z < y + z
theorem LO.Arith.mul_zero {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
x * 0 = 0
theorem LO.Arith.mul_one {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
x * 1 = x
theorem LO.Arith.mul_assoc {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) :
x * y * z = x * (y * z)
theorem LO.Arith.mul_comm {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) :
x * y = y * x
theorem LO.Arith.mul_lt_mul {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) :
x < y0 < zx * z < y * z
theorem LO.Arith.distr {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) :
x * (y + z) = x * y + x * z
theorem LO.Arith.lt_irrefl {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
¬x < x
theorem LO.Arith.lt_trans {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y z : M) :
x < yy < zx < z
theorem LO.Arith.lt_tri {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) :
x < y x = y y < x
theorem LO.Arith.zero_mul {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
0 * x = 0
Equations
  • One or more equations did not get rendered due to their size.
theorem LO.Arith.not_neg {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
¬x < 0
theorem LO.Arith.eq_succ_of_pos {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x : M} (h : 0 < x) :
∃ (y : M), x = y + 1
theorem LO.Arith.le_iff_lt_succ {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x y : M} :
x y x < y + 1
theorem LO.Arith.eq_nat_of_lt_nat {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n : } {x : M} :
x < n∃ (m : ), x = m