English
Let o be an ordinal, f a family of ordinals indexed below o, and c a regular cardinal. If lift(o.card) < c and f(i, hi) < ord(c) for all i, hi, then the bound-subscript supremum o.blsub f is below ord(c).
Русский
Пусть o — ординал, f — семейство ординалов для всех a < o, и c — регулярное кардинальное число. Если lift(o.card) < c и f(a, ha) < ord(c) для всех a < o и ha, тогда o.blsub f < ord(c).
LaTeX
$$$IsRegular(c) \land \operatorname{lift}(o.card) < c \Rightarrow \left( \forall a < o, \forall ha,\ f(a, ha) < \operatorname{ord}(c) \right) \Rightarrow \operatorname{blsub}(o,f) < \operatorname{ord}(c)$$$
Lean4
theorem blsub_lt_ord_lift_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
(ho : Cardinal.lift.{v, u} o.card < c) : (∀ i hi, f i hi < c.ord) → Ordinal.blsub.{u, v} o f < c.ord :=
blsub_lt_ord_lift (by rwa [hc.cof_eq])
