case h
α : Type u_1
E : Type ?u.19408
F : Type u_2
𝕜 : Type ?u.19414
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
x : F
⊢ ↑(weightedSMul μ ∅) x = ↑0 x
α : Type u_1
E : Type ?u.19408
F : Type u_2
𝕜 : Type ?u.19414
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
⊢ weightedSMul μ ∅ = 0
ext1 x
case h
α : Type u_1
E : Type ?u.19408
F : Type u_2
𝕜 : Type ?u.19414
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
x : F
⊢ ENNReal.toReal (↑↑μ ∅) • x = ↑0 x
case h
α : Type u_1
E : Type ?u.19408
F : Type u_2
𝕜 : Type ?u.19414
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
x : F
⊢ ↑(weightedSMul μ ∅) x = ↑0 x
rw [weightedSMul_apply]
no goals
case h
α : Type u_1
E : Type ?u.19408
F : Type u_2
𝕜 : Type ?u.19414
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
x : F
⊢ ENNReal.toReal (↑↑μ ∅) • x = ↑0 x
simp