cof_lsub_def_nonempty — Mathlib

English

For every ordinal o, the set {a : Cardinal | ∃ ι (f : ι → Ordinal), lsub f = o ∧ #ι = a} is nonempty.

Русский

Для каждого ординала o множество {a : Cardinal | ∃ ι, ∃ f : ι → Ordinal, lsub f = o ∧ #ι = a} не пусто.

LaTeX

$$$(o) : {a : Cardinal | \\exists (ι : _) (f : ι \\to Ordinal), lsub.f = o ∧ #ι = a}.Nonempty$$$

Lean4

/-- The set in the `lsub` characterization of `cof` is nonempty. -/
theorem cof_lsub_def_nonempty (o) : {a : Cardinal | ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a}.Nonempty :=
  ⟨_, card_mem_cof⟩

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