bsup_lt_ord_lift_of_isRegular — Mathlib

English

Let o be an ordinal and f a family of ordinals indexed below o. If c is regular and lift(o.card) < c and f(i, hi) < ord(c) for all i, hi, then o.bsup f < ord(c).

Русский

Пусть o — ординал, f — семейство ординалов с индексами ниже o. Если c регулярное и lift(o.card) < c и f(i, hi) < ord(c) для всех i, hi, то o.bsup f < ord(c).

LaTeX

$$$IsRegular(c) \land \operatorname{lift}(o.card) < c \Rightarrow ( \forall i, \forall hi,\ f(i, hi) < \operatorname{ord}(c) ) \Rightarrow \operatorname{bsup}(o,f) < \operatorname{ord}(c)$$$

Lean4

theorem bsup_lt_ord_lift_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} o.card < c) : (∀ i hi, f i hi < c.ord) → Ordinal.bsup.{u, v} o f < c.ord :=
  bsup_lt_ord_lift (by rwa [hc.cof_eq])

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