toElementarySubstructure — Mathlib

English

Bundles a substructure S satisfying TVT into an L-elementarySubstructure M.

Русский

Из подструктуры S, удовлетворяющей TVT, строится элементарная подструктура M.

LaTeX

$$$\text{toElementarySubstructure}(S,htv): L.ElementarySubstructure M$$$

Lean4

/-- Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure. -/
@[simps]
def toElementarySubstructure (S : L.Substructure M)
    (htv :
      ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → S) (a : M),
        φ.Realize default (Fin.snoc ((↑) ∘ x) a : _ → M) → ∃ b : S, φ.Realize default (Fin.snoc ((↑) ∘ x) b : _ → M)) :
    L.ElementarySubstructure M :=
  ⟨S, S.isElementary_of_exists htv⟩

Похожие утверждения