structure LO.FirstOrder.Structure.Model (L : LO.FirstOrder.Language) (M : Type u_1) : Type u_1

• intro : M

def LO.FirstOrder.Structure.Model.equiv (L : LO.FirstOrder.Language) (M : Type u_1) : M ≃ LO.FirstOrder.Structure.Model L M

Equations

• LO.FirstOrder.Structure.Model.equiv L M = { toFun := fun (x : M) => { intro := x }, invFun := LO.FirstOrder.Structure.Model.intro, left_inv := ⋯, right_inv := ⋯ }

instance LO.FirstOrder.Structure.Model.inst {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] : LO.FirstOrder.Structure L (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.inst = LO.FirstOrder.Structure.ofEquiv (LO.FirstOrder.Structure.Model.equiv L M)

instance LO.FirstOrder.Structure.Model.instNonempty {L : LO.FirstOrder.Language} {M : Type u_1} [h : Nonempty M] : Nonempty (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Structure.Model.elementaryEquiv (L : LO.FirstOrder.Language) (M : Type u_1) [Nonempty M] [LO.FirstOrder.Structure L M] : M ≡ₑ[L] LO.FirstOrder.Structure.Model L M

instance LO.FirstOrder.Structure.Model.instZeroOfZero {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Zero L] : Zero (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.instZeroOfZero = { zero := LO.FirstOrder.Semiterm.Operator.val op(0) ![] }

instance LO.FirstOrder.Structure.Model.instZero {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Zero L] : LO.FirstOrder.Structure.Zero L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Structure.Model.instOneOfOne {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.One L] : One (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.instOneOfOne = { one := LO.FirstOrder.Semiterm.Operator.val op(1) ![] }

instance LO.FirstOrder.Structure.Model.instOne {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.One L] : LO.FirstOrder.Structure.One L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Structure.Model.instAddOfAdd {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Add L] : Add (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.instAddOfAdd = { add := fun (x y : LO.FirstOrder.Structure.Model L M) => op(+).val ![x, y] }

instance LO.FirstOrder.Structure.Model.instAdd {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Add L] : LO.FirstOrder.Structure.Add L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Structure.Model.instMulOfMul {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Mul L] : Mul (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.instMulOfMul = { mul := fun (x y : LO.FirstOrder.Structure.Model L M) => op(*).val ![x, y] }

instance LO.FirstOrder.Structure.Model.instMul {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Mul L] : LO.FirstOrder.Structure.Mul L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Structure.Model.instExpOfExp {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Exp L] : Exp (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.instExpOfExp = { exp := fun (x : LO.FirstOrder.Structure.Model L M) => LO.FirstOrder.Semiterm.Operator.Exp.exp.val ![x] }

instance LO.FirstOrder.Structure.Model.instExp {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Exp L] : LO.FirstOrder.Structure.Exp L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Structure.Model.instEq {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Structure.Eq L M] : LO.FirstOrder.Structure.Eq L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Structure.Model.instLTOfLT {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.LT L] : LT (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.instLTOfLT = { lt := fun (x y : LO.FirstOrder.Structure.Model L M) => op(<).val ![x, y] }

instance LO.FirstOrder.Structure.Model.instLT {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.LT L] : LO.FirstOrder.Structure.LT L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Structure.Model.instMembershipOfMem {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Mem L] : Membership (LO.FirstOrder.Structure.Model L M) (LO.FirstOrder.Structure.Model L M)

Equations

• LO.FirstOrder.Structure.Model.instMembershipOfMem = { mem := fun (x y : LO.FirstOrder.Structure.Model L M) => op(∈).val ![x, y] }

instance LO.FirstOrder.Structure.Model.instMem {L : LO.FirstOrder.Language} {M : Type u_2} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Mem L] : LO.FirstOrder.Structure.Mem L (LO.FirstOrder.Structure.Model L M)

Equations

• ⋯ = ⋯

def LO.FirstOrder.Structure.ofFunc (F : ℕ → Type u_1) {M : Type u_2} (fF : {k : ℕ} → F k → (Fin k → M) → M) : LO.FirstOrder.Structure (LO.FirstOrder.Language.ofFunc F) M

Equations

• One or more equations did not get rendered due to their size.

theorem LO.FirstOrder.Structure.func_ofFunc (F : ℕ → Type u_1) {M : Type u_2} (fF : {k : ℕ} → F k → (Fin k → M) → M) {k : ℕ} (f : F k) (v : Fin k → M) : LO.FirstOrder.Structure.func f v = fF f v

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]

theorem LO.FirstOrder.Structure.func_sigma_inl {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {M : Type u_1} [str₁ : LO.FirstOrder.Structure L₁ M] [str₂ : LO.FirstOrder.Structure L₂ M] {k : ℕ} (f : L₁.Func k) (v : Fin k → M) : LO.FirstOrder.Structure.func (Sum.inl f) v = LO.FirstOrder.Structure.func f v

@[simp]

theorem LO.FirstOrder.Structure.func_sigma_inr {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {M : Type u_1} [str₁ : LO.FirstOrder.Structure L₁ M] [str₂ : LO.FirstOrder.Structure L₂ M] {k : ℕ} (f : L₂.Func k) (v : Fin k → M) : LO.FirstOrder.Structure.func (Sum.inr f) v = LO.FirstOrder.Structure.func f v

@[simp]

theorem LO.FirstOrder.Structure.rel_sigma_inl {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {M : Type u_1} [str₁ : LO.FirstOrder.Structure L₁ M] [str₂ : LO.FirstOrder.Structure L₂ M] {k : ℕ} (r : L₁.Rel k) (v : Fin k → M) : LO.FirstOrder.Structure.rel (Sum.inl r) v ↔ LO.FirstOrder.Structure.rel r v

@[simp]

theorem LO.FirstOrder.Structure.rel_sigma_inr {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {M : Type u_1} [str₁ : LO.FirstOrder.Structure L₁ M] [str₂ : LO.FirstOrder.Structure L₂ M] {k : ℕ} (r : L₂.Rel k) (v : Fin k → M) : LO.FirstOrder.Structure.rel (Sum.inr r) v ↔ LO.FirstOrder.Structure.rel r v

@[simp]

theorem LO.FirstOrder.Structure.val_lMap_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] {μ : Type u_2} {n : ℕ} (t : LO.FirstOrder.Semiterm L₁ μ n) (e : Fin n → M) (ε : μ → M) : LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.add L₁ L₂ M) e ε (LO.FirstOrder.Semiterm.lMap (LO.FirstOrder.Language.Hom.add₁ L₁ L₂) t) = LO.FirstOrder.Semiterm.val str₁ e ε t

@[simp]

theorem LO.FirstOrder.Structure.val_lMap_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] {μ : Type u_2} {n : ℕ} (t : LO.FirstOrder.Semiterm L₂ μ n) (e : Fin n → M) (ε : μ → M) : LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.add L₁ L₂ M) e ε (LO.FirstOrder.Semiterm.lMap (LO.FirstOrder.Language.Hom.add₂ L₁ L₂) t) = LO.FirstOrder.Semiterm.val str₂ e ε t

@[simp]

theorem LO.FirstOrder.Structure.eval_lMap_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] {μ : Type u_2} {n : ℕ} (p : LO.FirstOrder.Semiformula L₁ μ n) (e : Fin n → M) (ε : μ → M) : (LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.add L₁ L₂ M) e ε) ((LO.FirstOrder.Semiformula.lMap (LO.FirstOrder.Language.Hom.add₁ L₁ L₂)) p) ↔ (LO.FirstOrder.Semiformula.Eval str₁ e ε) p

@[simp]

theorem LO.FirstOrder.Structure.eval_lMap_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] {μ : Type u_2} {n : ℕ} (p : LO.FirstOrder.Semiformula L₂ μ n) (e : Fin n → M) (ε : μ → M) : (LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.add L₁ L₂ M) e ε) ((LO.FirstOrder.Semiformula.lMap (LO.FirstOrder.Language.Hom.add₂ L₁ L₂)) p) ↔ (LO.FirstOrder.Semiformula.Eval str₂ e ε) p

instance LO.FirstOrder.Structure.sigma {ι : Type u_2} (L : ι → LO.FirstOrder.Language) (M : Type u_1) [str : (i : ι) → LO.FirstOrder.Structure (L i) M] : LO.FirstOrder.Structure (LO.FirstOrder.Language.sigma L) M

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 k → M) : LO.FirstOrder.Structure.func ⟨i, f⟩ v = LO.FirstOrder.Structure.func f v

@[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 k → M) : LO.FirstOrder.Structure.rel ⟨i, r⟩ v ↔ LO.FirstOrder.Structure.rel r v

@[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 n → M) (ε : μ → M) : LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.sigma L M) e ε (LO.FirstOrder.Semiterm.lMap (LO.FirstOrder.Language.Hom.sigma L i) t) = LO.FirstOrder.Semiterm.val (str i) e ε t

@[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 n → M) (ε : μ → M) : (LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.sigma L M) e ε) ((LO.FirstOrder.Semiformula.lMap (LO.FirstOrder.Language.Hom.sigma L i)) p) ↔ (LO.FirstOrder.Semiformula.Eval (str i) e ε) p

instance LO.FirstOrder.instStructureULift {L : LO.FirstOrder.Language} {M : Type v} [LO.FirstOrder.Structure L M] : LO.FirstOrder.Structure L (ULift.{v', v} 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 k → ULift.{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.Structure.rel_uLift {L : LO.FirstOrder.Language} {M : Type v} [LO.FirstOrder.Structure L M] {k : ℕ} (r : L.Rel k) (v : Fin k → ULift.{v', v} M) : LO.FirstOrder.Structure.rel r v = LO.FirstOrder.Structure.rel r fun (i : Fin k) => (v i).down

theorem LO.FirstOrder.Semiterm.valm_uLift {L : LO.FirstOrder.Language} {M : Type v} [LO.FirstOrder.Structure L M] {n : ℕ} {ξ : Type u_1} {e : Fin n → ULift.{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 n → ULift.{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

theorem LO.FirstOrder.uLift_elementaryEquiv (L : LO.FirstOrder.Language) (M : Type v) [LO.FirstOrder.Structure L M] [Nonempty M] : ULift.{v', v} M ≡ₑ[L] M