α : Type u_1
E : Type ?u.79725
F : Type ?u.79728
𝕜 : Type ?u.79731
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ENNReal.toReal (↑↑μ s) * x
α : Type u_1
E : Type ?u.79725
F : Type ?u.79728
𝕜 : Type ?u.79731
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ↑(weightedSMul μ s) x
simp only [weightedSMul, Algebra.id.smul_eq_mul, coe_smul', id.def, coe_id', Pi.smul_apply]
no goals
α : Type u_1
E : Type ?u.79725
F : Type ?u.79728
𝕜 : Type ?u.79731
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ENNReal.toReal (↑↑μ s) * x
exact mul_nonneg toReal_nonneg hx