blsub_lt_ord_lift — Mathlib

English

If o.card lifted is less than c.cof and f bounds below c, then o.blsub f < c.

Русский

Если кардинал o поднят меньше cof(c) и f ограничены ниже c, то o.blsub f < c.

LaTeX

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

Lean4

theorem blsub_lt_ord_lift {o : Ordinal.{u}} {f : ∀ a < o, Ordinal} {c : Ordinal}
    (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ i hi, f i hi < c) : blsub.{u, v} o f < c :=
  lt_of_le_of_ne (blsub_le hf) fun h => ho.not_ge (by simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f)

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