ι : Sort u_1
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i => s i)) = sSup (Set.range fun i => ↑(s i))
ι : Sort u_1
s : ι → ℝ≥0
⊢ ↑(⨆ (i : ι), s i) = ⨆ (i : ι), ↑(s i)
rw [iSup, iSup, coe_sSup, ← Set.range_comp]
no goals
ι : Sort u_1
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i => s i)) = sSup (Set.range fun i => ↑(s i))
rfl