iSup_lt_ord_of_isRegular — Mathlib

English

Let c be a regular cardinal and ι a type with #ι < c. If every f(i) is strictly below ord(c), then the supremum of f over ι is strictly below ord(c).

Русский

Пусть c — регулярное кардинальное число и ι — тип с #ι < c. Если каждое f(i) строго меньше ord(c), то sup_i f(i) строго меньше ord(c).

LaTeX

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

Lean4

theorem iSup_lt_ord_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c.ord) → iSup f < c.ord :=
  iSup_lt_ord (by rwa [hc.cof_eq])

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