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