cof_iSup_le_lift — Mathlib

English

If each f(i) < iSup f, then cof(iSup f) ≤ lift(#ι).

Русский

Если для каждого i выполняется f(i) < iSup f, то cof(iSup f) ≤ lift(|ι|).

LaTeX

$$$\\forall {\\iota},\\forall f:\\iota\\to \\operatorname{Ordinal},\\ \\big( \\forall i, f(i) < \\operatorname{iSup}(f) \\big) \\Rightarrow \\operatorname{cof}(\\operatorname{iSup}(f)) \\le \\operatorname{lift}(\\#\\iota).$$$

Lean4

theorem cof_iSup_le_lift {ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) : cof (iSup f) ≤ Cardinal.lift.{v, u} #ι :=
  by
  rw [← iSup_eq_lsub_iff_lt_iSup] at H
  rw [H]
  exact cof_lsub_le_lift f

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