Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.Q.Basic

Supporting results for pointwise provable equality.

Robinson's theory $\mathsf{Q}$ #

source
inductive PointwiseComposition.FFL.FirstOrder.Arithmetic.RobinsonQ :
ArithmeticTheory

Data and laws for 𝐐 in 𝐐.

Instances For
    source
    def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐐» :
    Lean.ParserDescr

    The «term𝐐» construction in FFL.FirstOrder.Arithmetic.

    Equations
    Instances For
      source
      @[simp]
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.RobinsonQ.instModelsSetStrucORingSentenceStrNat :
      ℕ↓[β„’β‚’α΅£] ⊧* 𝐐
      source
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.RobinsonQ.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom :
      𝐄𝐐 β„’β‚’α΅£ β‰Ό 𝐐
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.succ_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (a : M) :
      a + 1 β‰  0
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.succ_inj {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a b : M} :
      a + 1 = b + 1 β†’ a = b
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a : M} :
      a + 0 = a
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (a b : M) :
      a + (b + 1) = a + b + 1
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (a : M) :
      a * 0 = 0
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (a b : M) :
      a * (b + 1) = a * b + a
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_or_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (a : M) :
      a = 0 ∨ βˆƒ (b : M), a = b + 1
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.exists_succ_of_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a : M} (ha : a β‰  0) :
      βˆƒ (b : M), a = b + 1
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.exists_succ_of_ne_zero' {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a : M} (ha : a β‰  0) :
      βˆƒ (b : M), b + 1 = a
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_def {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a b : M} :
      a < b ↔ βˆƒ (c : M), a + (c + 1) = b
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.one_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] :
      1 β‰  0
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.one_add_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] :
      1 + 0 = 1
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_add_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] :
      0 + 1 = 1
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.succ_inj_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a : M} :
      a + 1 = 1 β†’ a = 0
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_zero_of_eq_add_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a b : M} (h : a + b = 0) :
      a = 0 ∧ b = 0
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.one_mul_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] :
      1 * 1 = 1
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_mul_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] :
      0 * 1 = 0
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.not_le_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a : M} :
      Β¬a < 0
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_of_not_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a b : M} (ha : b β‰  0) :
      a < a + b
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.iff_le_one_eq_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {a : M} :
      a < 1 ↔ a = 0
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_zero_add {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (n : β„•) :
      0 + ORingStructure.numeral n = ORingStructure.numeral n
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_add_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (n : β„•) :
      ORingStructure.numeral n + 1 = ORingStructure.numeral (n + 1)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_add {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] (n m : β„•) :
      ORingStructure.numeral n + ORingStructure.numeral m = ORingStructure.numeral (n + m)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_zero_mul {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n : β„•} :
      0 * ORingStructure.numeral n = 0
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_mul_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n : β„•} :
      ORingStructure.numeral n * 1 = ORingStructure.numeral n
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_mul {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n m : β„•} :
      ORingStructure.numeral n * ORingStructure.numeral m = ORingStructure.numeral (n * m)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.exists_numeral_of_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n : β„•} (h : n β‰  0) :
      βˆƒ (m : β„•), ORingStructure.numeral n = ORingStructure.numeral (m + 1)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_zero_succ_ne {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n : β„•} :
      ORingStructure.numeral 0 β‰  ORingStructure.numeral (n + 1)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_succ_inj {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n m : β„•} (h : ORingStructure.numeral (n + 1) = ORingStructure.numeral (m + 1)) :
      ORingStructure.numeral n = ORingStructure.numeral m
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_ne_of_ne {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n m : β„•} (h : n β‰  m) :
      ORingStructure.numeral n β‰  ORingStructure.numeral m
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_lt_of_lt {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n m : β„•} (h : n < m) :
      ORingStructure.numeral n < ORingStructure.numeral m
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_lt_add {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n m : β„•} (hm : m β‰  0) :
      ORingStructure.numeral n < ORingStructure.numeral n + ORingStructure.numeral m
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_lt_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n : β„•} :
      ORingStructure.numeral n < ORingStructure.numeral n + ORingStructure.numeral 1
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.iff_lt_numeral_exists_numeral {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] {n : β„•} {x : M} :
      x < ORingStructure.numeral n ↔ βˆƒ m < n, x = ORingStructure.numeral m
      source
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.instModelsSetStrucORingSentenceStr {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐐] :
      M↓[β„’β‚’α΅£] ⊧* 𝐑₀
      source
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0RobinsonQ :
      𝐑₀ β‰Ό 𝐐
      source
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryR0RobinsonQ :
      𝐑₀ β‰Ί 𝐐