no goals
α : Type u_1
β : Type ?u.474375
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(restrict v Set.univ) i = ↑v i
rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]