Elementary Maps Between First-Order Structures

Main Definitions

• A FirstOrder.Language.ElementaryEmbedding is an embedding that commutes with the realizations of formulas.
• A FirstOrder.Language.ElementarySubstructure is a substructure where the realization of each formula agrees with the realization in the larger model.
• The FirstOrder.Language.elementaryDiagram of a structure is the set of all sentences with parameters that the structure satisfies.
• FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram is the canonical elementary embedding of any structure into a model of its elementary diagram.

Main Results

• The Tarski-Vaught Test for embeddings: FirstOrder.Language.Embedding.isElementary_of_exists gives a simple criterion for an embedding to be elementary.
• The Tarski-Vaught Test for substructures: FirstOrder.Language.Substructure.isElementary_of_exists gives a simple criterion for a substructure to be elementary.

structure FirstOrder.Language.ElementaryEmbedding (L : FirstOrder.Language) (M : Type u_1) (N : Type u_2) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : Type (max u_1 u_2)

• toFun : M → N
• map_formula' : ∀ ⦃n : ℕ⦄ (φ : FirstOrder.Language.Formula L (Fin n)) (x : Fin n → M), FirstOrder.Language.Formula.Realize φ (↑s ∘ x) ↔ FirstOrder.Language.Formula.Realize φ x

An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.

def FirstOrder.«term_↪ₑ[_]_» : Lean.TrailingParserDescr

An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.

instance FirstOrder.Language.ElementaryEmbedding.funLike {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FunLike (FirstOrder.Language.ElementaryEmbedding L M N) M fun x => N

instance FirstOrder.Language.ElementaryEmbedding.instCoeFunElementaryEmbeddingForAll {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : CoeFun (FirstOrder.Language.ElementaryEmbedding L M N) fun x => M → N

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_boundedFormula {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) {α : Type u_5} {n : ℕ} (φ : FirstOrder.Language.BoundedFormula L α n) (v : α → M) (xs : Fin n → M) : FirstOrder.Language.BoundedFormula.Realize φ (↑f ∘ v) (↑f ∘ xs) ↔ FirstOrder.Language.BoundedFormula.Realize φ v xs

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_formula {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) {α : Type u_5} (φ : FirstOrder.Language.Formula L α) (x : α → M) : FirstOrder.Language.Formula.Realize φ (↑f ∘ x) ↔ FirstOrder.Language.Formula.Realize φ x

theorem FirstOrder.Language.ElementaryEmbedding.map_sentence {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) (φ : FirstOrder.Language.Sentence L) : M ⊨ φ ↔ N ⊨ φ

theorem FirstOrder.Language.ElementaryEmbedding.theory_model_iff {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) (T : FirstOrder.Language.Theory L) : M ⊨ T ↔ N ⊨ T

theorem FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.ElementarilyEquivalent L M N

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.injective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) : Function.Injective ↑φ

instance FirstOrder.Language.ElementaryEmbedding.embeddingLike {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : EmbeddingLike (FirstOrder.Language.ElementaryEmbedding L M N) M N

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_fun {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M) : ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_rel {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M) : FirstOrder.Language.Structure.RelMap r (↑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x

instance FirstOrder.Language.ElementaryEmbedding.strongHomClass {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FirstOrder.Language.StrongHomClass L (FirstOrder.Language.ElementaryEmbedding L M N) M N

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_constants {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) (c : FirstOrder.Language.Constants L) : ↑φ ↑c = ↑c

def FirstOrder.Language.ElementaryEmbedding.toEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.Embedding L M N

An elementary embedding is also a first-order embedding.

def FirstOrder.Language.ElementaryEmbedding.toHom {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.Hom L M N

An elementary embedding is also a first-order homomorphism.

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.toEmbedding_toHom {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.Embedding.toHom (FirstOrder.Language.ElementaryEmbedding.toEmbedding f) = FirstOrder.Language.ElementaryEmbedding.toHom f

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.coe_toHom {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.ElementaryEmbedding L M N} : ↑(FirstOrder.Language.ElementaryEmbedding.toHom f) = ↑f

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.coe_toEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : ↑(FirstOrder.Language.ElementaryEmbedding.toEmbedding f) = ↑f

theorem FirstOrder.Language.ElementaryEmbedding.coe_injective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : Function.Injective FunLike.coe

theorem FirstOrder.Language.ElementaryEmbedding.ext {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] ⦃f : FirstOrder.Language.ElementaryEmbedding L M N⦄ ⦃g : FirstOrder.Language.ElementaryEmbedding L M N⦄ (h : ∀ (x : M), ↑f x = ↑g x) : f = g

theorem FirstOrder.Language.ElementaryEmbedding.ext_iff {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.ElementaryEmbedding L M N} {g : FirstOrder.Language.ElementaryEmbedding L M N} : f = g ↔ ∀ (x : M), ↑f x = ↑g x

def FirstOrder.Language.ElementaryEmbedding.refl (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] : FirstOrder.Language.ElementaryEmbedding L M M

The identity elementary embedding from a structure to itself

instance FirstOrder.Language.ElementaryEmbedding.instInhabitedElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Inhabited (FirstOrder.Language.ElementaryEmbedding L M M)

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.refl_apply {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (x : M) : ↑(FirstOrder.Language.ElementaryEmbedding.refl L M) x = x

def FirstOrder.Language.ElementaryEmbedding.comp {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (hnp : FirstOrder.Language.ElementaryEmbedding L N P) (hmn : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.ElementaryEmbedding L M P

Composition of elementary embeddings

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.comp_apply {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] (g : FirstOrder.Language.ElementaryEmbedding L N P) (f : FirstOrder.Language.ElementaryEmbedding L M N) (x : M) : ↑(FirstOrder.Language.ElementaryEmbedding.comp g f) x = ↑g (↑f x)

theorem FirstOrder.Language.ElementaryEmbedding.comp_assoc {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure L P] [FirstOrder.Language.Structure L Q] (f : FirstOrder.Language.ElementaryEmbedding L M N) (g : FirstOrder.Language.ElementaryEmbedding L N P) (h : FirstOrder.Language.ElementaryEmbedding L P Q) : FirstOrder.Language.ElementaryEmbedding.comp (FirstOrder.Language.ElementaryEmbedding.comp h g) f = FirstOrder.Language.ElementaryEmbedding.comp h (FirstOrder.Language.ElementaryEmbedding.comp g f)

Composition of elementary embeddings is associative.

@[inline, reducible]

abbrev FirstOrder.Language.elementaryDiagram (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] : FirstOrder.Language.Theory (FirstOrder.Language.withConstants L M)

The elementary diagram of an L-structure is the set of all sentences with parameters it satisfies.

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram_toFun (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] (N : Type u_5) [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure (FirstOrder.Language.withConstants L M) N] [FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L M) N] [N ⊨ FirstOrder.Language.elementaryDiagram L M] : ∀ (a : M), ↑(FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram L M N) a = (FirstOrder.Language.constantMap ∘ Sum.inr) a

def FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] (N : Type u_5) [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure (FirstOrder.Language.withConstants L M) N] [FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L M) N] [N ⊨ FirstOrder.Language.elementaryDiagram L M] : FirstOrder.Language.ElementaryEmbedding L M N

The canonical elementary embedding of an L-structure into any model of its elementary diagram

theorem FirstOrder.Language.Embedding.isElementary_of_exists {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) → ∃ b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))) {n : ℕ} (φ : FirstOrder.Language.Formula L (Fin n)) (x : Fin n → M) : FirstOrder.Language.Formula.Realize φ (↑f ∘ x) ↔ FirstOrder.Language.Formula.Realize φ x

The Tarski-Vaught test for elementarity of an embedding.

@[simp]

theorem FirstOrder.Language.Embedding.toElementaryEmbedding_toFun {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) → ∃ b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))) (a : M) : ↑(FirstOrder.Language.Embedding.toElementaryEmbedding f htv) a = ↑f a

def FirstOrder.Language.Embedding.toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) → ∃ b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))) : FirstOrder.Language.ElementaryEmbedding L M N

Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding.

def FirstOrder.Language.Equiv.toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : FirstOrder.Language.ElementaryEmbedding L M N

A first-order equivalence is also an elementary embedding.

@[simp]

theorem FirstOrder.Language.Equiv.toElementaryEmbedding_toEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : FirstOrder.Language.ElementaryEmbedding.toEmbedding (FirstOrder.Language.Equiv.toElementaryEmbedding f) = FirstOrder.Language.Equiv.toEmbedding f

@[simp]

theorem FirstOrder.Language.Equiv.coe_toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : ↑(FirstOrder.Language.Equiv.toElementaryEmbedding f) = ↑f

@[simp]

theorem FirstOrder.Language.realize_term_substructure {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {α : Type u_5} {S : FirstOrder.Language.Substructure L M} (v : α → { x // x ∈ S }) (t : FirstOrder.Language.Term L α) : FirstOrder.Language.Term.realize (Subtype.val ∘ v) t = ↑(FirstOrder.Language.Term.realize v t)

@[simp]

theorem FirstOrder.Language.Substructure.realize_boundedFormula_top {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {α : Type u_5} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n} {v : α → { x // x ∈ ⊤ }} {xs : Fin n → { x // x ∈ ⊤ }} : FirstOrder.Language.BoundedFormula.Realize φ v xs ↔ FirstOrder.Language.BoundedFormula.Realize φ (Subtype.val ∘ v) (Subtype.val ∘ xs)

@[simp]

theorem FirstOrder.Language.Substructure.realize_formula_top {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {α : Type u_5} {φ : FirstOrder.Language.Formula L α} {v : α → { x // x ∈ ⊤ }} : FirstOrder.Language.Formula.Realize φ v ↔ FirstOrder.Language.Formula.Realize φ (Subtype.val ∘ v)

def FirstOrder.Language.Substructure.IsElementary {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : Prop

A substructure is elementary when every formula applied to a tuple in the subtructure agrees with its value in the overall structure.

structure FirstOrder.Language.ElementarySubstructure (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] : Type u_1

• toSubstructure : FirstOrder.Language.Substructure L M
• isElementary' : FirstOrder.Language.Substructure.IsElementary ↑s

An elementary substructure is one in which every formula applied to a tuple in the subtructure agrees with its value in the overall structure.

instance FirstOrder.Language.ElementarySubstructure.instCoe {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Coe (FirstOrder.Language.ElementarySubstructure L M) (FirstOrder.Language.Substructure L M)

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

instance FirstOrder.Language.ElementarySubstructure.inducedStructure {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.Structure L { x // x ∈ S }

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.isElementary {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.Substructure.IsElementary ↑S

def FirstOrder.Language.ElementarySubstructure.subtype {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.ElementaryEmbedding L { x // x ∈ S } M

The natural embedding of an L.Substructure of M into M.

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.coeSubtype {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.ElementarySubstructure L M} : ↑(FirstOrder.Language.ElementarySubstructure.subtype S) = Subtype.val

instance FirstOrder.Language.ElementarySubstructure.instTop {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Top (FirstOrder.Language.ElementarySubstructure L M)

The substructure M of the structure M is elementary.

instance FirstOrder.Language.ElementarySubstructure.instInhabited {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Inhabited (FirstOrder.Language.ElementarySubstructure L M)

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.mem_top {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (x : M) : x ∈ ⊤

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.coe_top {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : ↑⊤ = Set.univ

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.realize_sentence {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) (φ : FirstOrder.Language.Sentence L) : { x // x ∈ S } ⊨ φ ↔ M ⊨ φ

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.theory_model_iff {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) (T : FirstOrder.Language.Theory L) : { x // x ∈ S } ⊨ T ↔ M ⊨ T

instance FirstOrder.Language.ElementarySubstructure.theory_model {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {T : FirstOrder.Language.Theory L} [h : M ⊨ T] {S : FirstOrder.Language.ElementarySubstructure L M} : { x // x ∈ S } ⊨ T

instance FirstOrder.Language.ElementarySubstructure.instNonempty {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] [Nonempty M] {S : FirstOrder.Language.ElementarySubstructure L M} : Nonempty { x // x ∈ S }

theorem FirstOrder.Language.ElementarySubstructure.elementarilyEquivalent {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.ElementarilyEquivalent L { x // x ∈ S } M

theorem FirstOrder.Language.Substructure.isElementary_of_exists {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → { x // x ∈ S }) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)) : FirstOrder.Language.Substructure.IsElementary S

The Tarski-Vaught test for elementarity of a substructure.

@[simp]

theorem FirstOrder.Language.Substructure.toElementarySubstructure_toSubstructure {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → { x // x ∈ S }) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)) : ↑(FirstOrder.Language.Substructure.toElementarySubstructure S htv) = S

def FirstOrder.Language.Substructure.toElementarySubstructure {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → { x // x ∈ S }) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)) : FirstOrder.Language.ElementarySubstructure L M

Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure.