blsub_succ_of_mono — Mathlib

English

If f is monotone with respect to the order, then blsub of succ o is equal to succ of blsub o.

Русский

Если f монотонна по порядку, то blsub на succ o равен succ от blsub o.

LaTeX

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

Lean4

theorem blsub_succ_of_mono {o : Ordinal.{u}} {f : ∀ a < succ o, Ordinal.{max u v}}
    (hf : ∀ {i j} (hi hj), i ≤ j → f i hi ≤ f j hj) : blsub.{_, v} _ f = succ (f o (lt_succ o)) :=
  bsup_succ_of_mono fun {_ _} hi hj h => succ_le_succ (hf hi hj h)

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