iInf_coe_lt_top — Mathlib

English

For a family f: ι → NNReal, the ENNReal infimum is strictly below top iff ι is nonempty; i.e. iInf over i of ENNReal.ofNNReal(f(i)) < top ↔ Nonempty ι.

Русский

Для семейства f: ι → NNReal инфимум ENNReal(ofNNReal(f(i))) строго меньше top тогда и только тогда, когда ι непусто.

LaTeX

$$$$\\mathrm{iInf}\\ i\\mapsto \\mathrm{ENNReal.ofNNReal}(f(i)) < \\top \\iff \\mathrm{Nonempty}\\ ι$$$$

Lean4

theorem iInf_coe_lt_top : ⨅ i, (f i : ℝ≥0∞) < ⊤ ↔ Nonempty ι :=
  WithTop.iInf_coe_lt_top

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