no goals
α : Type u_1
β : Type ?u.473341
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
hij : j ⊆ i
⊢ ↑(restrict v i) j = ↑v j
rw [restrict_apply v hi hj, Set.inter_eq_left_iff_subset.2 hij]