English
If κ is large enough relative to L and M is infinite, then M has an elementary extension N of cardinality κ.
Русский
Если κ достаточно велик относительно языка L и M бесконечно, то M имеет элементарное расширение N такой, что |N| = κ.
LaTeX
$$$\\exists N \\; (N \\text{ bundled L-structure},\\; M \\hookrightarrow_e N) \\land |N| = \\kappa.$$$
Lean4
/-- The **Upward Löwenheim–Skolem Theorem**: If `κ` is a cardinal greater than the cardinalities of
`L` and an infinite `L`-structure `M`, then `M` has an elementary extension of cardinality `κ`. -/
theorem exists_elementaryEmbedding_card_eq_of_ge (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w})
(h1 : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) (h2 : Cardinal.lift.{w} #M ≤ Cardinal.lift.{w'} κ) :
∃ N : Bundled L.Structure, Nonempty (M ↪ₑ[L] N) ∧ #N = κ :=
by
obtain ⟨N0, hN0⟩ := (L.elementaryDiagram M).exists_large_model_of_infinite_model κ M
rw [← lift_le.{max u v}, lift_lift, lift_lift] at h2
obtain ⟨N, ⟨NN0⟩, hN⟩ :=
exists_elementaryEmbedding_card_eq_of_le (L[[M]]) N0 κ
(aleph0_le_lift.1 ((aleph0_le_lift.2 (aleph0_le_mk M)).trans h2))
(by
simp only [card_withConstants, lift_add, lift_lift]
rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
rw [← lift_le.{w'}, lift_lift, lift_lift] at h1
exact ⟨h2, h1⟩)
(hN0.trans (by rw [← lift_umax, lift_id]))
letI := (lhomWithConstants L M).reduct N
haveI h : N ⊨ L.elementaryDiagram M := (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance
refine ⟨Bundled.of N, ⟨?_⟩, hN⟩
apply ElementaryEmbedding.ofModelsElementaryDiagram L M N
