iSup_lt — Mathlib

English

If cof bound is small, iSup of a family of cardinals is below c given pointwise bounds f i < c.

Русский

Если кофинальность ограничена, при покомпонентном ограничении f(i) < c, iSup f < c.

LaTeX

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

Lean4

theorem iSup_lt {ι} {f : ι → Cardinal} {c : Cardinal} (hι : #ι < c.ord.cof) : (∀ i, f i < c) → iSup f < c :=
  iSup_lt_lift (by rwa [(#ι).lift_id])

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