English
For a set s of ENNReal numbers with no ∞ in s, the toReal of the infimum equals the infimum of the toReal-images: (sInf s).toReal = sInf (ENNReal.toReal '' s).
Русский
Для множества s ENNReal без ∞ выполняется: (sInf s).toReal = sInf (ENNReal.toReal '' s).
LaTeX
$$$ (\mathrm{sInf}\ s).toReal = \mathrm{sInf}\ (\mathrm{ENNReal.toReal} '' s) $$$
Lean4
theorem toReal_sInf (s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) : (sInf s).toReal = sInf (ENNReal.toReal '' s) := by
simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]