bsup_succ_eq_blsub — Mathlib

English

The equality succ(bsup o f) = blsub o f holds iff there exists i < o with f(i, hi) = bsup o f.

Русский

Равенство succ(bsup o f) = blsub o f достигается тогда, когда найдется i < o такое, что f(i, hi) = bsup o f.

LaTeX

$$$ \\operatorname{succ}(\\operatorname{bsup}(o,f)) = \\operatorname{blsub}(o,f) \\iff \\exists i\\, \\exists hi, f(i,hi) = \\operatorname{bsup}(o,f) $$$

Lean4

theorem bsup_succ_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    succ (bsup.{_, v} o f) = blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f :=
  (blsub_le_bsup_succ f).ge_iff_eq'.symm.trans (bsup_succ_le_blsub f)

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