bsup_not_succ_of_ne_bsup — Mathlib

English

If every f(i,h) is not equal to bsup o f, then whenever a < bsup o f, its successor succ a is still below bsup o f.

Русский

Если все значения f(i,h) не равны bsup o f, то если a < bsup o f, то succ(a) < bsup o f.

LaTeX

$$$(\\forall {i} (h), f(i,h) \\neq \\operatorname{bsup}(o,f)) \\to (a < \\operatorname{bsup}(o,f) \\Rightarrow \\operatorname{succ}(a) < \\operatorname{bsup}(o,f))$$$

Lean4

theorem bsup_not_succ_of_ne_bsup {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}}
    (hf : ∀ {i : Ordinal} (h : i < o), f i h ≠ bsup.{_, v} o f) (a) : a < bsup.{_, v} o f → succ a < bsup.{_, v} o f :=
  by
  rw [← iSup_eq_bsup] at *
  exact succ_lt_iSup_of_ne_iSup fun i => hf _

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