iSup_lt_ord_lift — Mathlib

English

If lift(#ι) < cof(c) and ∀ i, f i < c, then iSup f < c.

Русский

Если lift(|ι|) < cof(c) и ∀ i, f(i) < c, тогда iSup f < c.

LaTeX

$$$\\operatorname{lift}(\\#\\iota) < \\operatorname{cof}(c) \\Rightarrow (\\forall i, f(i) < c) \\Rightarrow \\operatorname{iSup}(f) < c.$$$

Lean4

theorem iSup_lt_ord_lift {ι} {f : ι → Ordinal} {c : Ordinal} (hι : Cardinal.lift.{v, u} #ι < c.cof)
    (hf : ∀ i, f i < c) : iSup f < c :=
  (iSup_le_lsub f).trans_lt (lsub_lt_ord_lift hι hf)

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