α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(restrict (-w) i) j ≤ ↑(restrict (-v) i) j
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
⊢ restrict (-w) i ≤ restrict (-v) i
intro j hj₁
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ -↑w (j ∩ i) ≤ -↑v (j ∩ i)
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(restrict (-w) i) j ≤ ↑(restrict (-v) i) j
rw [restrict_apply _ hi hj₁, restrict_apply _ hi hj₁, neg_apply, neg_apply]
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑v (j ∩ i) ≤ ↑w (j ∩ i)
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ -↑w (j ∩ i) ≤ -↑v (j ∩ i)
refine' neg_le_neg _
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(restrict v i) j ≤ ↑(restrict w i) j
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑v (j ∩ i) ≤ ↑w (j ∩ i)
rw [← restrict_apply _ hi hj₁, ← restrict_apply _ hi hj₁]
no goals
α : Type u_1
β : Type ?u.548949
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(restrict v i) j ≤ ↑(restrict w i) j
exact h j hj₁