blsub_le_bsup_succ — Mathlib

English

Let o be an ordinal and f a function assigning to each a < o an ordinal. Then the Blsub value is bounded by the successor of the corresponding Bsub value: blsub(o, f) ≤ succ(bsup(o, f)).

Русский

Пусть o — ординал, а f — отображение, присваивающее каждому a < o ординал. Тогда значение Blsub ограничено следующим за BSup: blsub(o, f) ≤ succ(bsup(o, f)).

LaTeX

$$$ \\operatorname{blsub}(o,f) \\le \\operatorname{succ}(\\operatorname{bsup}(o,f)) $$$

Lean4

theorem blsub_le_bsup_succ {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    blsub.{_, v} o f ≤ succ (bsup.{_, v} o f) :=
  blsub_le fun i h => lt_succ_iff.2 (le_bsup f i h)

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