exists_lsub_cof — Mathlib

English

There exist an index set I and a function f:I → Ordinal such that lsub f = o and the cardinality of I equals cof(o).

Русский

Существуют индексное множество I и функция f:I → Ordinal такие, что lsub(f)=o и |I|=cof(o).

LaTeX

$$$\\exists I\\ \\exists f:I\\to \\operatorname{Ordinal}, \\ \\operatorname{lsub}(f)=o \\wedge \\#I=\\operatorname{cof}(o).$$$

Lean4

theorem exists_lsub_cof (o : Ordinal) : ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = cof o :=
  by
  rw [cof_eq_sInf_lsub]
  exact csInf_mem (cof_lsub_def_nonempty o)

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