English
Assume a nonempty index set ι and a real-valued function f on ι. Then in ENNReal the infimum commutes with ofReal: ENNReal.ofReal (⨅ i, f(i)) = ⨅ i, ENNReal.ofReal (f(i)).
Русский
Пусть индексное множество не пусто и есть функция f: ι → ℝ. Тогда в ENNReal infimum и ofReal коммутируют: ENNReal.ofReal (⨅ i, f(i)) = ⨅ i, ENNReal.ofReal (f(i)).
LaTeX
$$$ \mathrm{ENNReal}.ofReal\ (\inf_i f(i)) = \inf_i \mathrm{ENNReal}.ofReal\bigl(f(i)\bigr) $$$
Lean4
@[simp]
theorem ofReal_iInf [Nonempty ι] (f : ι → ℝ) : ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i) :=
by
obtain ⟨i, hi⟩ | h := em (∃ i, f i ≤ 0)
· rw [(iInf_eq_bot _).2 fun _ _ ↦ ⟨i, by simpa [ofReal_of_nonpos hi]⟩]
simp [Real.iInf_nonpos' ⟨i, hi⟩]
replace h i : 0 ≤ f i := le_of_not_ge fun hi ↦ h ⟨i, hi⟩
refine eq_of_forall_le_iff fun a ↦ ?_
obtain rfl | ha := eq_or_ne a ∞
· simp
rw [le_iInf_iff, le_ofReal_iff_toReal_le ha, le_ciInf_iff ⟨0, by simpa [mem_lowerBounds]⟩]
· exact forall_congr' fun i ↦ (le_ofReal_iff_toReal_le ha (h _)).symm
· exact Real.iInf_nonneg h
