English
For a family f: ι → NNReal, the supremum of ENNReal.ofNNReal(f(i)) equals top precisely when the range is not bounded above; i.e. ⨆ i, ENNReal.ofNNReal(f(i)) = ∞ iff not BddAbove (range f).
Русский
Для семейства f: ι → NNReal верхняя оболочка ENNReal.ofNNReal(f(i)) достигает ∞ тогда, когда множество значений не ограничено сверху; то есть ⨆ i ENNReal.ofNNReal(f(i)) = ∞ ⇔ не BddAbove (range f).
LaTeX
$$$$\\left(\\big\\uparrow(\\mathrm{iSup}\\ f)\\right) = \\top \\quad \\iff \\quad \\neg\\mathrm{BddAbove}(\\mathrm{range}\,f)$$$$
Lean4
theorem coe_iSup {ι : Sort*} {f : ι → ℝ≥0} (hf : BddAbove (range f)) : (↑(iSup f) : ℝ≥0∞) = ⨆ a, ↑(f a) :=
WithTop.coe_iSup _ hf
