iSup_lt_of_isRegular — Mathlib

English

If c is regular and lift(#ι) < c, and every f(i) < c, then iSup f < c.

Русский

Если c регулярное и lift(#ι) < c, и все f(i) < c, тогда iSup f < c.

LaTeX

$$$IsRegular(c) \land \operatorname{lift}(\#ι) < c \Rightarrow ( \forall i, f(i) < c ) \Rightarrow iSup(f) < c$$$

Lean4

theorem iSup_lt_of_isRegular {ι} {f : ι → Cardinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c) → iSup f < c :=
  iSup_lt (by rwa [hc.cof_eq])

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