iSup_coe_eq_top — Mathlib

English

For a family f: ι → NNReal, the ENNReal iSup over i of f(i) embedded equals top exactly when the range is not bounded above; i.e. ⨆ i ENNReal.ofNNReal(f(i)) = top ↔ ¬BddAbove(range f).

Русский

Для семейства f: ι → NNReal верхняя грань ENNReal.ofNNReal(f(i)) достигает верхнего элемента тогда и только тогда, когда множество значений не ограничено сверху.

LaTeX

$$$$\\big( \\big\\lceil \\mathrm{iSup}\\ i \\mapsto \\mathrm{ENNReal.ofNNReal}(f(i)) \\big\\rceil = \\top \\big) \\iff \\neg \\mathrm{BddAbove}(\\mathrm{range}\\ f)$$$$

Lean4

theorem iSup_coe_eq_top : ⨆ i, (f i : ℝ≥0∞) = ⊤ ↔ ¬BddAbove (range f) :=
  WithTop.iSup_coe_eq_top

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