exists_regular_cardinal_forall — Mathlib

English

For a small family X: ι → Type u with each X i small, there exists κ regular with HasCardinalLT (X i) κ for all i.

Русский

Для малого семейства X: ι → Type u и каждого i, X i мал, существует регулярный κ такой, что HasCardinalLT (X i) κ для всех i.

LaTeX

$$∃ κ, κ.IsRegular ∧ ∀ i, HasCardinalLT (X i) κ$$

Lean4

/-- For any `w`-small family `X : ι → Type u` of `w`-small types, there exists
a regular cardinal `κ : Cardinal.{w}` such that `HasCardinalLT (X i) κ` for all `i : ι`. -/
theorem exists_regular_cardinal_forall {ι : Type v} (X : ι → Type u) [Small.{w} ι] [∀ i, Small.{w} (X i)] :
    ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ :=
  by
  obtain ⟨κ, hκ, h⟩ := exists_regular_cardinal.{w} (Sigma X)
  exact ⟨κ, hκ, fun i ↦ h.of_injective _ sigma_mk_injective⟩

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