bsup_lt_ord_lift — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem bsup_lt_ord_lift {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : Cardinal.lift.{v, u} o.card < c.cof)
    (hf : ∀ i hi, f i hi < c) : bsup.{u, v} o f < c :=
  (bsup_le_blsub f).trans_lt (blsub_lt_ord_lift ho hf)

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