English
Given κ and M infinite, there exists a structure N of cardinality κ with an elementary embedding either N ↪ M or M ↪ N, with |N| = κ.
Русский
Пусть κ — кардинал и M бесконечна; существует структура N с |N| = κ и элементарное вложение либо N ↪ M, либо M ↪ N.
LaTeX
$$$\\exists N \\; ( (N \\hookrightarrow_e M) \\lor (M \\hookrightarrow_e N) ) \\land |N| = \\kappa.$$$
Lean4
/-- The Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the cardinalities of `L`
and an infinite `L`-structure `M`, then there is an elementary embedding in the appropriate
direction between then `M` and a structure of cardinality `κ`. -/
theorem exists_elementaryEmbedding_card_eq (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w})
(h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) :
∃ N : Bundled L.Structure, (Nonempty (N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] N)) ∧ #N = κ := by
cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M) with
| inl h =>
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
exact ⟨N, Or.inl hN1, hN2⟩
| inr h =>
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
exact ⟨N, Or.inr hN1, hN2⟩
