succ_lt_iSup_of_ne_iSup — Mathlib

English

If none of the f i equals iSup f, then from a < iSup f we get succ a < iSup f.

Русский

Если ни у одного f(i) не равно iSup f, то из a < iSup f следует succ a < iSup f.

LaTeX

$$∀ i, f i ≠ iSup f → ∀ {a}, a < iSup f → succ a < iSup f$$

Lean4

theorem succ_lt_iSup_of_ne_iSup {ι} {f : ι → Ordinal.{u}} [Small.{u} ι] (hf : ∀ i, f i ≠ iSup f) {a}
    (hao : a < iSup f) : succ a < iSup f := by
  by_contra! hoa
  exact
    hao.not_ge
      (Ordinal.iSup_le fun i ↦ le_of_lt_succ <| ((Ordinal.le_iSup _ _).lt_of_ne (hf i)).trans_le hoa)
        -- TODO: generalize to conditionally complete lattices.

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