bsup_eq_blsub_of_lt_succ_limit — Mathlib

English

If o is a succ-limit ordinal and f increases along successors, then bsup o f = blsub o f.

Русский

Если o — предел-сукцесса и f возрастает по переходам к следующему, то bsup o f = blsub o f.

LaTeX

$$$ \\text{IsSuccLimit}(o) \\; \\Rightarrow \\; \\operatorname{bsup}(o,f) = \\operatorname{blsub}(o,f) \\quad \\text{under monotonicity hypothesis } hf$$$

Lean4

theorem bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : IsSuccLimit o) {f : ∀ a < o, Ordinal.{max u v}}
    (hf : ∀ a ha, f a ha < f (succ a) (ho.succ_lt ha)) : bsup.{_, v} o f = blsub.{_, v} o f :=
  by
  rw [bsup_eq_blsub_iff_lt_bsup]
  exact fun i hi => (hf i hi).trans_le (le_bsup f _ _)

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