no goals
α : Type u_1
β : Type ?u.592052
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬MeasurableSet i
⊢ restrict v i ≤ restrict 0 i
rw [restrict_zero, restrict_not_measurable _ hi]