α : Type u_1
E : Type u_2
F : Type ?u.210759
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s : Set α
h : ↑↑μ s ≠ ⊤
this : Fact (↑↑μ s < ⊤)
⊢ (ENNReal.toReal (↑↑μ s) • ⨍ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.210759
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s : Set α
h : ↑↑μ s ≠ ⊤
⊢ (ENNReal.toReal (↑↑μ s) • ⨍ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
haveI := Fact.mk h.lt_top
no goals
α : Type u_1
E : Type u_2
F : Type ?u.210759
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s : Set α
h : ↑↑μ s ≠ ⊤
this : Fact (↑↑μ s < ⊤)
⊢ (ENNReal.toReal (↑↑μ s) • ⨍ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
rw [← measure_smul_average, restrict_apply_univ]