toReal_iInf — Mathlib

English

If f(i) ≠ ∞ for all i, then the Real-valued infimum commutes with toReal: (iInf f).toReal = ⨅ i, (f i).toReal.

Русский

Если f(i) не равны ∞ для всех i, то предел кReal коммутирует с toReal: (iInf f).toReal = ⨅ i, (f i).toReal.

LaTeX

$$$ (\!iInf\ f).toReal = \!\bigl( \inf_i f(i) \bigr).toReal $$$

Lean4

theorem toReal_iInf (hf : ∀ i, f i ≠ ∞) : (iInf f).toReal = ⨅ i, (f i).toReal := by
  simp only [ENNReal.toReal, toNNReal_iInf hf, NNReal.coe_iInf]

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