exists_model_card_eq — Mathlib

English

If T has an infinite model, there exists a model N of T with cardinality κ.

Русский

Если у теории T есть бесконечная модель, существует модель N T с кардиналностью κ.

LaTeX

$$$\\exists N: ModelType_{T}, \\#N = \\kappa.$$$

Lean4

theorem exists_model_card_eq (h : ∃ M : ModelType.{u, v, max u v} T, Infinite M) (κ : Cardinal.{w}) (h1 : ℵ₀ ≤ κ)
    (h2 : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) : ∃ N : ModelType.{u, v, w} T, #N = κ := by
  cases h with
  | intro M MI =>
    obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
    haveI : Nonempty N := hN.nonempty
    exact ⟨hN.theory_model.bundled, rfl⟩

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