α : Type u_1
β : Type ?u.545966
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
j : Set α
a✝ : MeasurableSet j
⊢ ↑(restrict v ∅) j ≤ ↑(restrict w ∅) j
α : Type u_1
β : Type ?u.545966
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ restrict v ∅ ≤ restrict w ∅
intro j _
no goals
α : Type u_1
β : Type ?u.545966
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
j : Set α
a✝ : MeasurableSet j
⊢ ↑(restrict v ∅) j ≤ ↑(restrict w ∅) j
rw [restrict_empty, restrict_empty]