structure LO.FirstOrder.Structure.Hom (L : LO.FirstOrder.Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : Type (max u_2 u_3)

• toFun : M₁ → M₂
• func' : ∀ {k : ℕ} (f : L.Func k) (v : Fin k → M₁), self.toFun (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (self.toFun ∘ v)
• rel' : ∀ {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (self.toFun ∘ v)

theorem LO.FirstOrder.Structure.Hom.func' {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (self : M₁ →ₛ[L] M₂) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : self.toFun (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (self.toFun ∘ v)

theorem LO.FirstOrder.Structure.Hom.rel' {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (self : M₁ →ₛ[L] M₂) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (self.toFun ∘ v)

def LO.FirstOrder.Structure.«term_→ₛ[_]_» : Lean.TrailingParserDescr

Equations

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

structure LO.FirstOrder.Structure.Embedding (L : LO.FirstOrder.Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] extends LO.FirstOrder.Structure.Hom : Type (max u_2 u_3)

• toFun : M₁ → M₂
• func' : ∀ {k : ℕ} (f : L.Func k) (v : Fin k → M₁), self.toFun (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (self.toFun ∘ v)
• rel' : ∀ {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (self.toFun ∘ v)
• toFun_inj : Function.Injective self.toFun
• rel_inv' : ∀ {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r (self.toFun ∘ v) → LO.FirstOrder.Structure.rel r v

theorem LO.FirstOrder.Structure.Embedding.toFun_inj {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (self : M₁ ↪ₛ[L] M₂) : Function.Injective self.toFun

theorem LO.FirstOrder.Structure.Embedding.rel_inv' {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (self : M₁ ↪ₛ[L] M₂) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : LO.FirstOrder.Structure.rel r (self.toFun ∘ v) → LO.FirstOrder.Structure.rel r v

def LO.FirstOrder.Structure.«term_↪ₛ[_]_» : Lean.TrailingParserDescr

Equations

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

structure LO.FirstOrder.Structure.Iso (L : LO.FirstOrder.Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] extends LO.FirstOrder.Structure.Embedding : Type (max u_2 u_3)

• toFun : M₁ → M₂
• func' : ∀ {k : ℕ} (f : L.Func k) (v : Fin k → M₁), self.toFun (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (self.toFun ∘ v)
• rel' : ∀ {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (self.toFun ∘ v)
• toFun_inj : Function.Injective self.toFun
• rel_inv' : ∀ {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r (self.toFun ∘ v) → LO.FirstOrder.Structure.rel r v
• toFun_bij : Function.Bijective self.toFun

theorem LO.FirstOrder.Structure.Iso.toFun_bij {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (self : M₁ ≃ₛ[L] M₂) : Function.Bijective self.toFun

def LO.FirstOrder.Structure.«term_≃ₛ[_]_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.Structure.ClosedSubset.ext {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} (x : LO.FirstOrder.Structure.ClosedSubset L M) (y : LO.FirstOrder.Structure.ClosedSubset L M) (domain : x.domain = y.domain) : x = y

theorem LO.FirstOrder.Structure.ClosedSubset.ext_iff {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} (x : LO.FirstOrder.Structure.ClosedSubset L M) (y : LO.FirstOrder.Structure.ClosedSubset L M) : x = y ↔ x.domain = y.domain

structure LO.FirstOrder.Structure.ClosedSubset (L : LO.FirstOrder.Language) (M : Type u_1) [s : LO.FirstOrder.Structure L M] : Type u_1

• domain : Set M
• domain_closed : ∀ {k : ℕ} (f : L.Func k) {v : Fin k → M}, (∀ (i : Fin k), v i ∈ self.domain) → LO.FirstOrder.Structure.func f v ∈ self.domain

theorem LO.FirstOrder.Structure.ClosedSubset.domain_closed {L : LO.FirstOrder.Language} {M : Type u_1} [s : LO.FirstOrder.Structure L M] (self : LO.FirstOrder.Structure.ClosedSubset L M) {k : ℕ} (f : L.Func k) {v : Fin k → M} : (∀ (i : Fin k), v i ∈ self.domain) → LO.FirstOrder.Structure.func f v ∈ self.domain

class LO.FirstOrder.Structure.HomClass (F : Type u_5) (L : outParam LO.FirstOrder.Language) (M₁ : outParam (Type u_6)) (M₂ : outParam (Type u_7)) [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] : Type

• map_func : ∀ (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁), h (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (⇑h ∘ v)
• map_rel : ∀ (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (⇑h ∘ v)

theorem LO.FirstOrder.Structure.HomClass.map_func {F : Type u_5} {L : outParam LO.FirstOrder.Language} {M₁ : outParam (Type u_6)} {M₂ : outParam (Type u_7)} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] [self : LO.FirstOrder.Structure.HomClass F L M₁ M₂] (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : h (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (⇑h ∘ v)

theorem LO.FirstOrder.Structure.HomClass.map_rel {F : Type u_5} {L : outParam LO.FirstOrder.Language} {M₁ : outParam (Type u_6)} {M₂ : outParam (Type u_7)} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] [self : LO.FirstOrder.Structure.HomClass F L M₁ M₂] (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (⇑h ∘ v)

class LO.FirstOrder.Structure.EmbeddingClass (F : Type u_5) (L : outParam LO.FirstOrder.Language) (M₁ : outParam (Type u_6)) (M₂ : outParam (Type u_7)) [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] extends LO.FirstOrder.Structure.HomClass : Type

• map_func : ∀ (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁), h (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (⇑h ∘ v)
• map_rel : ∀ (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (⇑h ∘ v)
• map_inj : ∀ (f : F), Function.Injective ⇑f
• map_rel_inv : ∀ (f : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r (⇑f ∘ v) → LO.FirstOrder.Structure.rel r v

theorem LO.FirstOrder.Structure.EmbeddingClass.map_inj {F : Type u_5} {L : outParam LO.FirstOrder.Language} {M₁ : outParam (Type u_6)} {M₂ : outParam (Type u_7)} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] [self : LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂] (f : F) : Function.Injective ⇑f

theorem LO.FirstOrder.Structure.EmbeddingClass.map_rel_inv {F : Type u_5} {L : outParam LO.FirstOrder.Language} {M₁ : outParam (Type u_6)} {M₂ : outParam (Type u_7)} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] [self : LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂] (f : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : LO.FirstOrder.Structure.rel r (⇑f ∘ v) → LO.FirstOrder.Structure.rel r v

class LO.FirstOrder.Structure.IsoClass (F : Type u_5) (L : outParam LO.FirstOrder.Language) (M₁ : outParam (Type u_6)) (M₂ : outParam (Type u_7)) [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] extends LO.FirstOrder.Structure.EmbeddingClass : Type

• map_func : ∀ (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁), h (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (⇑h ∘ v)
• map_rel : ∀ (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (⇑h ∘ v)
• map_inj : ∀ (f : F), Function.Injective ⇑f
• map_rel_inv : ∀ (f : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁), LO.FirstOrder.Structure.rel r (⇑f ∘ v) → LO.FirstOrder.Structure.rel r v
• map_bij : ∀ (f : F), Function.Bijective ⇑f

theorem LO.FirstOrder.Structure.IsoClass.map_bij {F : Type u_5} {L : outParam LO.FirstOrder.Language} {M₁ : outParam (Type u_6)} {M₂ : outParam (Type u_7)} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [FunLike F M₁ M₂] [self : LO.FirstOrder.Structure.IsoClass F L M₁ M₂] (f : F) : Function.Bijective ⇑f

instance LO.FirstOrder.Structure.instFunLikeHom {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : FunLike (M₁ →ₛ[L] M₂) M₁ M₂

Equations

• LO.FirstOrder.Structure.instFunLikeHom = { coe := fun (φ : M₁ →ₛ[L] M₂) => φ.toFun, coe_injective' := ⋯ }

instance LO.FirstOrder.Structure.instHomClassHom {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : LO.FirstOrder.Structure.HomClass (M₁ →ₛ[L] M₂) L M₁ M₂

Equations

• LO.FirstOrder.Structure.instHomClassHom = { map_func := ⋯, map_rel := ⋯ }

theorem LO.FirstOrder.Structure.Hom.ext {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (φ : M₁ →ₛ[L] M₂) (ψ : M₁ →ₛ[L] M₂) (h : ∀ (x : M₁), φ x = ψ x) : φ = ψ

theorem LO.FirstOrder.Structure.HomClass.ext {M₁ : Type u_2} {M₂ : Type u_3} {F : Type u_5} [FunLike F M₁ M₂] (φ : F) (ψ : F) (h : ∀ (x : M₁), φ x = ψ x) : φ = ψ

theorem LO.FirstOrder.Structure.HomClass.func {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.HomClass F L M₁ M₂] (φ : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : φ (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (⇑φ ∘ v)

theorem LO.FirstOrder.Structure.HomClass.rel {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.HomClass F L M₁ M₂] (φ : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : LO.FirstOrder.Structure.rel r v → LO.FirstOrder.Structure.rel r (⇑φ ∘ v)

theorem LO.FirstOrder.Structure.HomClass.val_term {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.HomClass F L M₁ M₂] (φ : F) {n : ℕ} {ξ : Type u_6} (e : Fin n → M₁) (ε : ξ → M₁) (t : LO.FirstOrder.Semiterm L ξ n) : φ (LO.FirstOrder.Semiterm.val s₁ e ε t) = LO.FirstOrder.Semiterm.val s₂ (⇑φ ∘ e) (⇑φ ∘ ε) t

instance LO.FirstOrder.Structure.instFunLikeEmbedding {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : FunLike (M₁ ↪ₛ[L] M₂) M₁ M₂

Equations

• LO.FirstOrder.Structure.instFunLikeEmbedding = { coe := fun (φ : M₁ ↪ₛ[L] M₂) => φ.toFun, coe_injective' := ⋯ }

instance LO.FirstOrder.Structure.instEmbeddingClassEmbedding {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : LO.FirstOrder.Structure.EmbeddingClass (M₁ ↪ₛ[L] M₂) L M₁ M₂

Equations

• LO.FirstOrder.Structure.instEmbeddingClassEmbedding = LO.FirstOrder.Structure.EmbeddingClass.mk ⋯ ⋯

theorem LO.FirstOrder.Structure.Embedding.ext {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (φ : M₁ ↪ₛ[L] M₂) (ψ : M₁ ↪ₛ[L] M₂) (h : ∀ (x : M₁), φ x = ψ x) : φ = ψ

def LO.FirstOrder.Structure.EmbeddingClass.toEmbedding {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂] (φ : F) : M₁ ↪ M₂

Equations

• LO.FirstOrder.Structure.EmbeddingClass.toEmbedding φ = { toFun := ⇑φ, inj' := ⋯ }

theorem LO.FirstOrder.Structure.EmbeddingClass.func {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂] (φ : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : φ (LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f (⇑φ ∘ v)

theorem LO.FirstOrder.Structure.EmbeddingClass.rel {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂] (φ : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : LO.FirstOrder.Structure.rel r (⇑φ ∘ v) ↔ LO.FirstOrder.Structure.rel r v

instance LO.FirstOrder.Structure.instFunLikeIso {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : FunLike (M₁ ≃ₛ[L] M₂) M₁ M₂

Equations

• LO.FirstOrder.Structure.instFunLikeIso = { coe := fun (φ : M₁ ≃ₛ[L] M₂) => φ.toFun, coe_injective' := ⋯ }

instance LO.FirstOrder.Structure.instIsoClassIso {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : LO.FirstOrder.Structure.IsoClass (M₁ ≃ₛ[L] M₂) L M₁ M₂

Equations

• LO.FirstOrder.Structure.instIsoClassIso = LO.FirstOrder.Structure.IsoClass.mk ⋯

theorem LO.FirstOrder.Structure.Iso.ext {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (φ : M₁ ≃ₛ[L] M₂) (ψ : M₁ ≃ₛ[L] M₂) (h : ∀ (x : M₁), φ x = ψ x) : φ = ψ

instance LO.FirstOrder.Structure.ClosedSubset.instSetLike {L : LO.FirstOrder.Language} {M : Type u_1} [s : LO.FirstOrder.Structure L M] : SetLike (LO.FirstOrder.Structure.ClosedSubset L M) M

Equations

• LO.FirstOrder.Structure.ClosedSubset.instSetLike = { coe := LO.FirstOrder.Structure.ClosedSubset.domain, coe_injective' := ⋯ }

theorem LO.FirstOrder.Structure.ClosedSubset.closed {L : LO.FirstOrder.Language} {M : Type u_1} [s : LO.FirstOrder.Structure L M] (u : LO.FirstOrder.Structure.ClosedSubset L M) {k : ℕ} (f : L.Func k) {v : Fin k → M} (hv : ∀ (i : Fin k), v i ∈ u) : LO.FirstOrder.Structure.func f v ∈ u

instance LO.FirstOrder.Structure.ClosedSubset.toStructure {L : LO.FirstOrder.Language} {M : Type u_1} [s : LO.FirstOrder.Structure L M] (u : LO.FirstOrder.Structure.ClosedSubset L M) : LO.FirstOrder.Structure L ↥u

Equations

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

theorem LO.FirstOrder.Structure.ClosedSubset.func {L : LO.FirstOrder.Language} {M : Type u_1} [s : LO.FirstOrder.Structure L M] (u : LO.FirstOrder.Structure.ClosedSubset L M) {k : ℕ} (f : L.Func k) (v : Fin k → ↥u) : ↑(LO.FirstOrder.Structure.func f v) = LO.FirstOrder.Structure.func f fun (i : Fin k) => ↑(v i)

theorem LO.FirstOrder.Structure.ClosedSubset.rel {L : LO.FirstOrder.Language} {M : Type u_1} [s : LO.FirstOrder.Structure L M] (u : LO.FirstOrder.Structure.ClosedSubset L M) {k : ℕ} (r : L.Rel k) (v : Fin k → ↥u) : LO.FirstOrder.Structure.rel r v ↔ LO.FirstOrder.Structure.rel r fun (i : Fin k) => ↑(v i)

def LO.FirstOrder.Structure.ClosedSubset.inclusion {L : LO.FirstOrder.Language} {M : Type u_1} [s : LO.FirstOrder.Structure L M] (u : LO.FirstOrder.Structure.ClosedSubset L M) : ↥u ↪ₛ[L] M

Equations

• u.inclusion = { toFun := Subtype.val, func' := ⋯, rel' := ⋯, toFun_inj := ⋯, rel_inv' := ⋯ }

theorem LO.FirstOrder.Semiformula.eval_hom_iff_of_open {ξ : Type u_6} {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂] (φ : F) {n : ℕ} {e₁ : Fin n → M₁} {ε₁ : ξ → M₁} {p : LO.FirstOrder.Semiformula L ξ n} : p.Open → ((LO.FirstOrder.Semiformula.Eval s₁ e₁ ε₁) p ↔ (LO.FirstOrder.Semiformula.Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p)

theorem LO.FirstOrder.Semiformula.eval_hom_univClosure {ξ : Type u_6} {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [LO.FirstOrder.Structure.EmbeddingClass F L M₁ M₂] (φ : F) {n : ℕ} {ε₁ : ξ → M₁} {p : LO.FirstOrder.Semiformula L ξ n} (hp : p.Open) : (LO.FirstOrder.Semiformula.Evalf s₂ (⇑φ ∘ ε₁)) (∀* p) → (LO.FirstOrder.Semiformula.Evalf s₁ ε₁) (∀* p)

def LO.FirstOrder.Structure.ElementaryEquiv (L : LO.FirstOrder.Language) (M₁ : Type u_2) (M₂ : Type u_3) [Nonempty M₁] [Nonempty M₂] [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : Prop

Equations

• (M₁ ≡ₑ[L] M₂) = ∀ (p : LO.FirstOrder.SyntacticFormula L), M₁ ⊧ₘ p ↔ M₂ ⊧ₘ p

def LO.FirstOrder.Structure.«term_≡ₑ[_]_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.Structure.ElementaryEquiv.refl {L : LO.FirstOrder.Language} (M : Type u_5) [Nonempty M] [LO.FirstOrder.Structure L M] : M ≡ₑ[L] M

theorem LO.FirstOrder.Structure.ElementaryEquiv.symm {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] : (M₁ ≡ₑ[L] M₂) → M₂ ≡ₑ[L] M₁

theorem LO.FirstOrder.Structure.ElementaryEquiv.trans {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [Nonempty M₁] [Nonempty M₂] [Nonempty M₃] [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] [s₃ : LO.FirstOrder.Structure L M₃] : (M₁ ≡ₑ[L] M₂) → (M₂ ≡ₑ[L] M₃) → M₁ ≡ₑ[L] M₃

theorem LO.FirstOrder.Structure.ElementaryEquiv.models {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (h : M₁ ≡ₑ[L] M₂) {p : LO.FirstOrder.SyntacticFormula L} : M₁ ⊧ₘ p ↔ M₂ ⊧ₘ p

theorem LO.FirstOrder.Structure.ElementaryEquiv.modelsTheory {L : LO.FirstOrder.Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : LO.FirstOrder.Structure L M₁] [s₂ : LO.FirstOrder.Structure L M₂] (h : M₁ ≡ₑ[L] M₂) {T : LO.FirstOrder.Theory L} : M₁ ⊧ₘ* T ↔ M₂ ⊧ₘ* T

theorem LO.FirstOrder.Structure.ElementaryEquiv.ofEquiv {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {N : Type u_5} [Nonempty N] (φ : M ≃ N) : M ≡ₑ[L] N