English
If a theory T has an infinite model, then for every cardinal κ there exists a model N of T whose cardinality is at least κ.
Русский
Если теория T имеет бесконечную модель, то для любого кардинального числа κ существует модель N теории T такая, что |N| ≥ κ.
LaTeX
$$$\\forall \\kappa \\in \\mathrm{Card},\\; \\exists N \\text{ such that } N \\models T \\text{ and } \\kappa \\le |N|$$$
Lean4
/-- Any theory with an infinite model has arbitrarily large models. -/
theorem exists_large_model_of_infinite_model (T : L.Theory) (κ : Cardinal.{w}) (M : Type w') [L.Structure M] [M ⊨ T]
[Infinite M] : ∃ N : ModelType.{_, _, max u v w} T, Cardinal.lift.{max u v w} κ ≤ #N :=
by
obtain ⟨N⟩ := isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M
refine ⟨(N.is_model.mono Set.subset_union_left).bundled.reduct _, ?_⟩
haveI : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono Set.subset_union_right
rw [ModelType.reduct_Carrier, coe_of]
refine _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) ?_
rw [← mk_univ]
refine (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{max u v w}.1 ?_)
rw [lift_lift]
