Elementary

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)

Imported declaration from the Incompleteness formalization.

• toFun : M₁ → M₂

  Imported declaration from the Incompleteness formalization.

• 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

Imported declaration from the Incompleteness formalization.

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)

Imported declaration from the Incompleteness formalization.

• 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

Imported declaration from the Incompleteness formalization.

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)

Imported declaration from the Incompleteness formalization.

• 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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

• domain : Set M

  Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

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

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

Imported declaration from the Incompleteness formalization.

• 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

Imported declaration from the Incompleteness formalization.

• 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

Imported declaration from the Incompleteness formalization.

• 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 s₁ e ε t) = Semiterm.val s₂ (⇑φ ∘ 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₂

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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} : φ.Open → ((Eval s₁ e₁ ε₁) φ ↔ (Eval s₂ (⇑Θ ∘ e₁) (⇑Θ ∘ ε₁)) φ)

theorem LO.FirstOrder.Semiformula.eval_hom_univClosure {ξ : 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 s₂ (⇑Θ ∘ ε₁)) (∀* φ) → (Evalf s₁ ε₁) (∀* φ)

def 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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem 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.models {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₂) {φ : SyntacticFormula L} : M₁ ⊧ₘ φ ↔ 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₁ ⊧ₘ* T ↔ M₂ ⊧ₘ* 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