English
For an infinite structure M and a cardinal κ with suitable bounds, there exists a structure N of cardinality κ and an elementary embedding N ↪ₑ M.
Русский
Для бесконечной структуры M и кардинала κ при заданных пределах существует структура N такова, что |N| = κ и существует элементарное вложение N ↪ₑ M.
LaTeX
$$$\\exists N \\; (N \\text{ bundled L-structure},\\; N \\hookrightarrow_e M) \\land |N| = \\kappa.$$$
Lean4
/-- A version of The Downward Löwenheim–Skolem theorem where the structure `N` elementarily embeds
into `M`, but is not by type a substructure of `M`, and thus can be chosen to belong to the universe
of the cardinal `κ`.
-/
theorem exists_elementaryEmbedding_card_eq_of_le (M : Type w') [L.Structure M] [Nonempty M] (κ : Cardinal.{w})
(h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) (h3 : lift.{w'} κ ≤ Cardinal.lift.{w} #M) :
∃ N : Bundled L.Structure, Nonempty (N ↪ₑ[L] M) ∧ #N = κ :=
by
obtain ⟨S, _, hS⟩ := exists_elementarySubstructure_card_eq L ∅ κ h1 (by simp) h2 h3
have : Small.{w} S := by
rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS
exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')
refine
⟨(equivShrink S).bundledInduced L, ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
lift_inj.1 (_root_.trans ?_ hS)⟩
simp only [Equiv.bundledInduced_α, lift_mk_shrink']
