toNNReal_iInf — Mathlib

English

Let f be a family of ENNReal indexed by ι such that every f(i) ≠ ∞. Then the NNReal value of the infimum equals the infimum of the NNReal values: (iInf f).toNNReal = ⨅ i, (f i).toNNReal.

Русский

Пусть f: ι → ENNReal такой, что все f(i) ≠ ∞. Тогда nnReal-образ минимального элемента равен инфимууму nnReal-образов: (iInf f).toNNReal = ⨅ i, (f i).toNNReal.

LaTeX

$$$ (\inf_i f(i)).\!toNNReal = \inf_i (f(i).toNNReal) $$$

Lean4

theorem toNNReal_iInf (hf : ∀ i, f i ≠ ∞) : (iInf f).toNNReal = ⨅ i, (f i).toNNReal :=
  by
  cases isEmpty_or_nonempty ι
  · rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]
  · lift f to ι → ℝ≥0 using hf
    simp_rw [← coe_iInf, toNNReal_coe]

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