bsup_lt_ord_of_isRegular — Mathlib

English

If o.card < c and c is regular, and f(i, hi) < ord(c) for all i, hi, then o.bsup f < ord(c).

Русский

Если o.card < c и c регулярное, и f(i, hi) < ord(c) для всех i, hi, то o.bsup f < ord(c).

LaTeX

$$$IsRegular(c) \land o.card < c \Rightarrow ( \forall i, \forall hi,\ f(i, hi) < \operatorname{ord}(c) ) \Rightarrow \operatorname{bsup}(o,f) < \operatorname{ord}(c)$$$

Lean4

theorem bsup_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c) (hι : o.card < c) :
    (∀ i hi, f i hi < c.ord) → Ordinal.bsup o f < c.ord :=
  bsup_lt_ord (by rwa [hc.cof_eq])

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