iInf_coe_eq_top — Mathlib

English

For a family f: ι → NNReal, the ENNReal of the infimum equals top if and only if ι is empty; i.e. iInf over i of ENNReal.ofNNReal(f(i)) = top ↔ IsEmpty ι.

Русский

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

LaTeX

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

Lean4

theorem iInf_coe_eq_top : ⨅ i, (f i : ℝ≥0∞) = ⊤ ↔ IsEmpty ι :=
  WithTop.iInf_coe_eq_top

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