ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (↑a * ⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), ↑(a * f i)
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (a * ⨆ (i : ι), f i) = ⨆ (i : ι), a * f i
rw [← NNReal.coe_eq, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]
no goals
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (↑a * ⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), ↑(a * f i)
exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _