iSup_coe_lt_top — Mathlib

English

For a family f: ι → NNReal, the ENNReal lt relation at the iSup level is equivalent to boundedness of range; i.e. iSup of ENNReal.ofNNReal(f(i)) < top iff range f is bounded above.

Русский

Для семейства f: ι → NNReal, отношение меньше верхнего элемента на уровне iSup эквивалентно ограниченности множества значений; i.e. iSup ENNReal.ofNNReal(f(i)) < top ⇔ range f ограничено сверху.

LaTeX

$$$$\\operatorname{lt} (\\mathrm{iSup}\\ i\\mapsto \\mathrm{ENNReal.ofNNReal}(f(i)), \\top) \\iff \\mathrm{BddAbove}(\\mathrm{range}\\ f)$$$$

Lean4

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

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