English
If all r ∈ s satisfy r ≠ ∞, then (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s).
Русский
Пусть все r ∈ s удовлетворяют r ≠ ∞; тогда (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s).
LaTeX
$$$ (\mathrm{sSup}\ s).toNNReal = \mathrm{sSup}\bigl( \mathrm{ENNReal.toNNReal} '' s \bigr) $$$
Lean4
theorem toNNReal_sSup (s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) : (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s) :=
by
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
simpa only [← sSup_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iSup hf)