Documentation

Foundation.FirstOrder.Arith.PeanoMinus

source
def LO.Arith.instLE_foundation {M : Type u_1} [LO.ORingStruc M] :
LE M
Equations
  • LO.Arith.instLE_foundation = { le := fun (x y : M) => x = y ∨ x < y }
Instances For
    source
    theorem LO.Arith.le_def {M : Type u_1} [LO.ORingStruc M] {x : M} {y : M} :
    x ≤ y ↔ x = y ∨ x < y
    source
    theorem LO.Arith.add_zero {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
    x + 0 = x
    source
    theorem LO.Arith.add_assoc {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :
    x + y + z = x + (y + z)
    source
    theorem LO.Arith.add_comm {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :
    x + y = y + x
    source
    theorem LO.Arith.add_eq_of_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :
    x < y → ∃ (z : M), x + z = y
    source
    @[simp]
    theorem LO.Arith.zero_le {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
    0 ≤ x
    source
    theorem LO.Arith.zero_lt_one {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
    0 < 1
    source
    theorem LO.Arith.one_le_of_zero_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
    0 < x → 1 ≤ x
    source
    theorem LO.Arith.add_lt_add {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :
    x < y → x + z < y + z
    source
    theorem LO.Arith.mul_zero {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
    x * 0 = 0
    source
    theorem LO.Arith.mul_one {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
    x * 1 = x
    source
    theorem LO.Arith.mul_assoc {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :
    x * y * z = x * (y * z)
    source
    theorem LO.Arith.mul_comm {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :
    x * y = y * x
    source
    theorem LO.Arith.mul_lt_mul {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :
    x < y → 0 < z → x * z < y * z
    source
    theorem LO.Arith.distr {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :
    x * (y + z) = x * y + x * z
    source
    theorem LO.Arith.lt_irrefl {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
    ¬x < x
    source
    theorem LO.Arith.lt_trans {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :
    x < y → y < z → x < z
    source
    theorem LO.Arith.lt_tri {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :
    x < y ∨ x = y ∨ y < x
    source
    def LO.Arith.instAddCommMonoid_foundation {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
    AddCommMonoid M
    Equations
    Instances For
      source
      def LO.Arith.instCommMonoid_foundation {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
      CommMonoid M
      Equations
      Instances For
        source
        def LO.Arith.instLinearOrder_foundation {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
        LinearOrder M
        Equations
        • LO.Arith.instLinearOrder_foundation = LinearOrder.mk ⋯ (fun (x x_1 : M) => Classical.dec ((fun (x x_2 : M) => x ≤ x_2) x x_1)) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯
        Instances For
          source
          theorem LO.Arith.zero_mul {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
          0 * x = 0
          source
          def LO.Arith.instLinearOrderedCommSemiring_foundation {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
          LinearOrderedCommSemiring M
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def LO.Arith.instCanonicallyOrderedAddCommMonoid_foundation {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
            CanonicallyOrderedAddCommMonoid M
            Equations
            Instances For
              source
              theorem LO.Arith.numeral_eq_natCast {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (n : ℕ) :
              LO.ORingStruc.numeral n = ↑n
              source
              theorem LO.Arith.not_neg {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :
              ¬x < 0
              source
              theorem LO.Arith.eq_succ_of_pos {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x : M} (h : 0 < x) :
              ∃ (y : M), x = y + 1
              source
              theorem LO.Arith.le_iff_lt_succ {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x : M} {y : M} :
              x ≤ y ↔ x < y + 1
              source
              theorem LO.Arith.eq_nat_of_lt_nat {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n : ℕ} {x : M} :
              x < ↑n → ∃ (m : ℕ), x = ↑m
              source
              instance LO.FirstOrder.Arith.CobhamR0.subTheoryPAMinus :
              𝐑₀ ≼ 𝐏𝐀⁻
              Equations