Documentation

Foundation.FirstOrder.Basic.Model

  • intro : M
Instances For
    Equations
    Instances For
      Equations
      Equations
      Equations
      • LO.FirstOrder.Structure.Model.instExpOfExp = { exp := fun (x : LO.FirstOrder.Structure.Model L M) => LO.FirstOrder.Semiterm.Operator.Exp.exp.val ![x] }
      Equations
      def LO.FirstOrder.Structure.ofFunc (F : Type u_1) {M : Type u_2} (fF : {k : } → F k(Fin kM)M) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem LO.FirstOrder.Structure.func_ofFunc (F : Type u_1) {M : Type u_2} (fF : {k : } → F k(Fin kM)M) {k : } (f : F k) (v : Fin kM) :
        instance LO.FirstOrder.Structure.add (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) (M : Type u_1) [str₁ : LO.FirstOrder.Structure L₁ M] [str₂ : LO.FirstOrder.Structure L₂ M] :
        LO.FirstOrder.Structure (L₁.add L₂) M
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem LO.FirstOrder.Structure.func_sigma {ι : Type u_3} (L : ιLO.FirstOrder.Language) (M : Type u_1) [str : (i : ι) → LO.FirstOrder.Structure (L i) M] {i : ι} {k : } (f : (L i).Func k) (v : Fin kM) :
        @[simp]
        theorem LO.FirstOrder.Structure.rel_sigma {ι : Type u_3} (L : ιLO.FirstOrder.Language) (M : Type u_1) [str : (i : ι) → LO.FirstOrder.Structure (L i) M] {i : ι} {k : } (r : (L i).Rel k) (v : Fin kM) :
        @[simp]
        theorem LO.FirstOrder.Structure.val_lMap_sigma {ι : Type u_4} (L : ιLO.FirstOrder.Language) (M : Type u_1) [str : (i : ι) → LO.FirstOrder.Structure (L i) M] {i : ι} {μ : Type u_2} {n : } (t : LO.FirstOrder.Semiterm (L i) μ n) (e : Fin nM) (ε : μM) :
        @[simp]
        theorem LO.FirstOrder.Structure.eval_lMap_sigma {ι : Type u_4} (L : ιLO.FirstOrder.Language) (M : Type u_1) [str : (i : ι) → LO.FirstOrder.Structure (L i) M] {i : ι} {μ : Type u_2} {n : } (p : LO.FirstOrder.Semiformula (L i) μ n) (e : Fin nM) (ε : μM) :
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem LO.FirstOrder.Structure.func_uLift {L : LO.FirstOrder.Language} {M : Type v} [LO.FirstOrder.Structure L M] {k : } (f : L.Func k) (v : Fin kULift.{v', v} M) :
        LO.FirstOrder.Structure.func f v = { down := LO.FirstOrder.Structure.func f fun (i : Fin k) => (v i).down }
        @[simp]
        theorem LO.FirstOrder.Semiterm.valm_uLift {L : LO.FirstOrder.Language} {M : Type v} [LO.FirstOrder.Structure L M] {n : } {ξ : Type u_1} {e : Fin nULift.{v', v} M} {ε : ξULift.{v', v} M} {t : LO.FirstOrder.Semiterm L ξ n} :
        LO.FirstOrder.Semiterm.valm (ULift.{v', v} M) e ε t = { down := LO.FirstOrder.Semiterm.valm M (fun (i : Fin n) => (e i).down) (fun (i : ξ) => (ε i).down) t }
        theorem LO.FirstOrder.Semiformula.evalm_uLift {L : LO.FirstOrder.Language} {M : Type v} [LO.FirstOrder.Structure L M] {n : } {ξ : Type u_1} {e : Fin nULift.{v', v} M} {ε : ξULift.{v', v} M} {p : LO.FirstOrder.Semiformula L ξ n} :
        (LO.FirstOrder.Semiformula.Evalm (ULift.{v', v} M) e ε) p (LO.FirstOrder.Semiformula.Evalm M (fun (i : Fin n) => (e i).down) fun (i : ξ) => (ε i).down) p