isElementary_of_exists — Mathlib

English

The substructure S is elementary if it satisfies the TVT condition with respect to M.

Русский

Подструктура S является элементарной, если она удовлетворяет тесту TVT относительно M.

LaTeX

$$$S.IsElementary\;\text{ follows from TVT} \;htv$$$

Lean4

/-- The Tarski-Vaught test for elementarity of a substructure. -/
theorem isElementary_of_exists (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)) :
    S.IsElementary := fun _ => S.subtype.isElementary_of_exists htv

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