Documentation

Foundation.FirstOrder.Arith.Basic

class LO.ORingStruc (α : Type u_1) extends Zero , One , Add , Mul , LT :
Type u_1
    Instances
      instance LO.instORingStrucOfZeroOfOneOfAddOfMulOfLT {α : Type u_1} [Zero α] [One α] [Add α] [Mul α] [LT α] :
      Equations
      • LO.instORingStrucOfZeroOfOneOfAddOfMulOfLT = LO.ORingStruc.mk
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem LO.FirstOrder.Language.oringEmb_zero {L : LO.FirstOrder.Language} [L.ORing] :
        LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Zero.zero = LO.FirstOrder.Language.Zero.zero
        @[simp]
        theorem LO.FirstOrder.Language.oringEmb_one {L : LO.FirstOrder.Language} [L.ORing] :
        LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.One.one = LO.FirstOrder.Language.One.one
        @[simp]
        theorem LO.FirstOrder.Language.oringEmb_add {L : LO.FirstOrder.Language} [L.ORing] :
        LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Add.add = LO.FirstOrder.Language.Add.add
        @[simp]
        theorem LO.FirstOrder.Language.oringEmb_mul {L : LO.FirstOrder.Language} [L.ORing] :
        LO.FirstOrder.Language.oringEmb.func LO.FirstOrder.Language.Mul.mul = LO.FirstOrder.Language.Mul.mul
        @[simp]
        theorem LO.FirstOrder.Language.oringEmb_eq {L : LO.FirstOrder.Language} [L.ORing] :
        LO.FirstOrder.Language.oringEmb.rel op(=) = op(=)
        @[simp]
        theorem LO.FirstOrder.Language.oringEmb_lt {L : LO.FirstOrder.Language} [L.ORing] :
        LO.FirstOrder.Language.oringEmb.rel op(<) = op(<)
        Equations
        @[simp]
        theorem LO.FirstOrder.Semiterm.oringEmb_add {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : } (v : Fin 2LO.FirstOrder.Semiterm ℒₒᵣ ξ n) :
        LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (op(+).operator v) = (‘(!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) + !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))’)
        @[simp]
        theorem LO.FirstOrder.Semiterm.oringEmb_mul {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : } (v : Fin 2LO.FirstOrder.Semiterm ℒₒᵣ ξ n) :
        LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (op(*).operator v) = ‘(!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) * !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))’
        Equations
        Equations
        @[simp]
        theorem LO.FirstOrder.Semiformula.oringEmb_eq {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : } (v : Fin 2LO.FirstOrder.Semiterm ℒₒᵣ ξ n) :
        (LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) (op(=).operator v) = (“!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) = !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))
        @[simp]
        theorem LO.FirstOrder.Semiformula.oringEmb_lt {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : } (v : Fin 2LO.FirstOrder.Semiterm ℒₒᵣ ξ n) :
        (LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) (op(<).operator v) = (“!!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 0)) < !!(LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb (v 1)))
        @[reducible, inline]
        Equations
        Instances For
          def LO.FirstOrder.Semiformula.ballLTSucc {L : LO.FirstOrder.Language} [L.LT] [L.Zero] [L.One] [L.Add] {ξ : Type u_1} {n : } (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) :
          Equations
          Instances For
            def LO.FirstOrder.Semiformula.bexLTSucc {L : LO.FirstOrder.Language} [L.LT] [L.Zero] [L.One] [L.Add] {ξ : Type u_1} {n : } (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) :
            Equations
            Instances For
              theorem LO.FirstOrder.Semiformula.eval_bexLTSucc {n : } {L : LO.FirstOrder.Language} [L.LT] [L.Zero] [L.One] [L.Add] {ξ : Type u_1} {M : Type u_2} {s : LO.FirstOrder.Structure L M} [LT M] [One M] [Add M] [LO.FirstOrder.Structure.LT L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {e : Fin nM} {ε : ξM} :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem LO.FirstOrder.Arith.consequence_of {L : LO.FirstOrder.Language} [L.ORing] (T : LO.FirstOrder.Theory L) [𝐄𝐐 T] (p : LO.FirstOrder.SyntacticFormula L) (H : ∀ (M : Type (max u w)) [inst : LO.ORingStruc M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : LO.FirstOrder.Structure.ORing L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ p) :
                  T p
                  Equations
                  • LO.FirstOrder.Arith.instGoedelNumberORingOfEncodable = LO.FirstOrder.Semiterm.Operator.GoedelNumber.ofEncodable
                  Equations