lsub_lt_ord_of_isRegular — Mathlib

English

If hc is regular and hι : #ι < c, and ∀ i, f i < c.ord, then lsub f < c.ord.

Русский

Если hc регулярный и hι : #ι < c, и для всех i, f i < c.ord, то lsub f < c.ord.

LaTeX

$$$(\forall i, f(i) < c.ord) \rightarrow Ordinal.lsub(f) < c.ord.$$$

Lean4

theorem lsub_lt_ord_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c.ord) → Ordinal.lsub f < c.ord :=
  lsub_lt_ord (by rwa [hc.cof_eq])

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