ciSup_eq_univ_of_not_bddAbove — Mathlib

English

If range f is not bounded above, then the supremum over i of f i equals the supremum of the whole space.

Русский

Если диапазон f не ограничен сверху, то супремум по i от f(i) равен супремуму всего пространства.

LaTeX

$$$ \neg BddAbove(\mathrm{range}(f)) \Rightarrow \big( \big( \sup_i f(i) \big) = sSup \mathrm{univ} \big)$$$

Lean4

theorem ciSup_eq_univ_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup univ :=
  csSup_eq_univ_of_not_bddAbove hf

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