exists_elementarilyEquivalent_card_eq

English

There exists a structure N of cardinality κ that is elementarily equivalent to M.

Русский

Существует структура N с |N| = κ, элементарно эквивалентная M.

LaTeX

$$$\\exists N: (M \\equiv_L N) \\land |N| = \\kappa.$$$

Lean4

/-- A consequence of the Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the
cardinalities of `L` and an infinite `L`-structure `M`, then there is a structure of cardinality `κ`
elementarily equivalent to `M`. -/
theorem exists_elementarilyEquivalent_card_eq (M : Type w') [L.Structure M] [Infinite M] (κ : Cardinal.{w})
    (h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) :
    ∃ N : CategoryTheory.Bundled L.Structure, (M ≅[L] N) ∧ #N = κ :=
  by
  obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2
  · exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩
  · exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩

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