blsub_lt_ord_of_isRegular — Mathlib

English

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

Русский

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

LaTeX

$$$IsRegular(c) \land o.card < c \Rightarrow ( \forall a < o, \forall ha,\ f(a, ha) < \operatorname{ord}(c) ) \Rightarrow \operatorname{blsub}(o,f) < \operatorname{ord}(c)$$$

Lean4

theorem blsub_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c) (ho : o.card < c) :
    (∀ i hi, f i hi < c.ord) → Ordinal.blsub o f < c.ord :=
  blsub_lt_ord (by rwa [hc.cof_eq])

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