toElementaryEmbedding — Mathlib

English

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

Русский

Из вложения, удовлетворяющего тесту Тарски–Воутта, строится элементарное L-вложение.

LaTeX

$$$\exists e: M \hookrightarrow_L N,\ e \text{ является элементарным вложением и } e \text{ совпадает с } f$$$

Lean4

/-- Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding. -/
@[simps]
def toElementaryEmbedding (f : M ↪[L] N)
    (htv :
      ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
        φ.Realize default (Fin.snoc (f ∘ x) a : _ → N) → ∃ b : M, φ.Realize default (Fin.snoc (f ∘ x) (f b) : _ → N)) :
    M ↪ₑ[L] N :=
  ⟨f, fun _ => f.isElementary_of_exists htv⟩

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