bsup_lt_ord — Mathlib

English

If o.card < c.cof and ∀ i, f(i) < c, then bsup(o,f) < c.

Русский

Если o.card < cof(c) и ∀ i, f(i) < c, тогда bsup(o,f) < c.

LaTeX

$$$\\forall o\\,\\forall f:\\, o.card < c.cof \\rightarrow (\\forall i, f(i) < c) \\rightarrow \\operatorname{bsup}(o,f) < c.$$$

Lean4

theorem bsup_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o.card < c.cof) :
    (∀ i hi, f i hi < c) → bsup.{u, u} o f < c :=
  bsup_lt_ord_lift (by rwa [o.card.lift_id])

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