exists_regular_cardinal — Mathlib

English

For any type X there exists a regular cardinal κ with HasCardinalLT X κ.

Русский

Для любого типа X существует регулярный кардинал κ such that HasCardinalLT X κ.

LaTeX

$$∃ κ, κ.IsRegular ∧ HasCardinalLT X κ$$

Lean4

/-- For any `w`-small type `X`, there exists a regular cardinal `κ : Cardinal.{w}`
such that `HasCardinalLT X κ`. -/
theorem exists_regular_cardinal (X : Type u) [Small.{w} X] : ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ HasCardinalLT X κ :=
  ⟨Order.succ (max (Cardinal.mk (Shrink.{w} X)) .aleph0), Cardinal.isRegular_succ (le_max_right _ _), by
    simp [hasCardinalLT_iff_of_equiv (equivShrink.{w} X), hasCardinalLT_iff_cardinal_mk_lt]⟩

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