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

• toFun : M₁ → M₂
• func' {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : self.toFun (func f v) = func f (self.toFun ∘ v)
• rel' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → 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 : Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : Structure L M₁] [s₂ : Structure L M₂] extends M₁ →ₛ[L] M₂ : Type (max u_2 u_3)

• toFun : M₁ → M₂
• func' {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : self.toFun (func f v) = func f (self.toFun ∘ v)
• rel' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → rel r (self.toFun ∘ v)
• toFun_inj : Function.Injective self.toFun
• rel_inv' {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r (self.toFun ∘ v) → 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 : Language) (M₁ : Type u_2) (M₂ : Type u_3) [s₁ : Structure L M₁] [s₂ : Structure L M₂] extends M₁ ↪ₛ[L] M₂ : Type (max u_2 u_3)

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

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

Equations

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

structure LO.FirstOrder.Structure.ClosedSubset (L : Language) (M : Type u_1) [s : 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) → func f v ∈ self.domain

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

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

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

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

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

• map_func (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : h (func f v) = func f (⇑h ∘ v)
• map_rel (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → 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₁) : rel r (⇑f ∘ v) → rel r v

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

• map_func (h : F) {k : ℕ} (f : L.Func k) (v : Fin k → M₁) : h (func f v) = func f (⇑h ∘ v)
• map_rel (h : F) {k : ℕ} (r : L.Rel k) (v : Fin k → M₁) : rel r v → 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₁) : rel r (⇑f ∘ v) → rel r v
• map_bij (f : F) : Function.Bijective ⇑f

@[implicit_reducible]

instance LO.FirstOrder.Structure.instFunLikeHom {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : 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 : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] : HomClass (M₁ →ₛ[L] M₂) L M₁ M₂

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

theorem LO.FirstOrder.Structure.Hom.ext_iff {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {φ ψ : M₁ →ₛ[L] M₂} : φ = ψ ↔ ∀ (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) (h : ∀ (x : M₁), φ x = ψ x) : φ = ψ

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

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

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

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

@[implicit_reducible]

instance LO.FirstOrder.Structure.instFunLikeEmbedding {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : 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 : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] : EmbeddingClass (M₁ ↪ₛ[L] M₂) L M₁ M₂

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

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

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

Equations

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

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

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

@[implicit_reducible]

instance LO.FirstOrder.Structure.instFunLikeIso {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : 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 : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] : IsoClass (M₁ ≃ₛ[L] M₂) L M₁ M₂

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

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

@[implicit_reducible]

instance LO.FirstOrder.Structure.ClosedSubset.instSetLike {L : Language} {M : Type u_1} [s : Structure L M] : SetLike (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 : Language} {M : Type u_1} [s : Structure L M] (u : ClosedSubset L M) {k : ℕ} (f : L.Func k) {v : Fin k → M} (hv : ∀ (i : Fin k), v i ∈ u) : func f v ∈ u

@[implicit_reducible]

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

Equations

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

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

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

def LO.FirstOrder.Structure.ClosedSubset.inclusion {L : Language} {M : Type u_1} [s : Structure L M] (u : 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 : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {F : Type u_5} [FunLike F M₁ M₂] [Structure.EmbeddingClass F L M₁ M₂] (Θ : F) {n : ℕ} {e₁ : Fin n → M₁} {ε₁ : ξ → M₁} {φ : Semiformula L ξ n} (h : φ.Open) : (Eval e₁ ε₁) φ ↔ (Eval (⇑Θ ∘ e₁) (⇑Θ ∘ ε₁)) φ

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

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

• models {φ : Sentence L} : M₁↓[L] ⊧ φ ↔ M₂↓[L] ⊧ φ

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

Equations

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

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

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

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

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

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

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

theorem LO.FirstOrder.Structure.ElementaryEquiv.val_eq_of_equiv {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {ξ : Type u_5} {n : ℕ} {f₁ : ξ → M₁} {f₂ : ξ → M₂} {b₁ : Fin n → M₁} {b₂ : Fin n → M₂} (I : M₁ ≃ M₂) (hf : ∀ (x : ξ), I (f₁ x) = f₂ x) (hb : ∀ (x : Fin n), I (b₁ x) = b₂ x) (hfunc : ∀ {k : ℕ} (f : L.Func k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → I (func f v₁) = func f v₂) (t : Semiterm L ξ n) : I (Semiterm.val b₁ f₁ t) = Semiterm.val b₂ f₂ t

theorem LO.FirstOrder.Structure.ElementaryEquiv.eval_iff_of_equiv {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [s₁ : Structure L M₁] [s₂ : Structure L M₂] {ξ : Type u_5} {n : ℕ} {f₁ : ξ → M₁} {f₂ : ξ → M₂} {b₁ : Fin n → M₁} {b₂ : Fin n → M₂} (I : M₁ ≃ M₂) (hf : ∀ (x : ξ), I (f₁ x) = f₂ x) (hb : ∀ (x : Fin n), I (b₁ x) = b₂ x) (hrel : ∀ {k : ℕ} (R : L.Rel k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → (rel R v₁ ↔ rel R v₂)) (hfunc : ∀ {k : ℕ} (f : L.Func k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → I (func f v₁) = func f v₂) (φ : Semiformula L ξ n) : (Semiformula.Eval b₁ f₁) φ ↔ (Semiformula.Eval b₂ f₂) φ

theorem LO.FirstOrder.Structure.ElementaryEquiv.of_equiv {L : Language} {M₁ : Type u_2} {M₂ : Type u_3} [Nonempty M₁] [Nonempty M₂] [s₁ : Structure L M₁] [s₂ : Structure L M₂] (I : M₁ ≃ M₂) (hrel : ∀ {k : ℕ} (R : L.Rel k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → (rel R v₁ ↔ rel R v₂)) (hfunc : ∀ {k : ℕ} (f : L.Func k) {v₁ : Fin k → M₁} {v₂ : Fin k → M₂}, (∀ (i : Fin k), I (v₁ i) = v₂ i) → I (func f v₁) = func f v₂) : M₁ ≡ₑ[L] M₂