no goals
α : Type u_2
β : Type ?u.116823
E : Type u_1
F : Type ?u.116829
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
c : E
⊢ (∫ (x : α) in s, c ∂μ) = ENNReal.toReal (↑↑μ s) • c
rw [integral_const, Measure.restrict_apply_univ]