case pos
α : Type u_1
β : Type ?u.543897
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ ↑v j ≤ ↑w j

case neg
α : Type u_1
β : Type ?u.543897
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ ↑v j ≤ ↑w j
α : Type u_1
β : Type ?u.543897
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
⊢ ↑v j ≤ ↑w j
by_cases hj₁ : MeasurableSet j
no goals
case pos
α : Type u_1
β : Type ?u.543897
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ ↑v j ≤ ↑w j
exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj
no goals
case neg
α : Type u_1
β : Type ?u.543897
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ ↑v j ≤ ↑w j
rw [v.not_measurable hj₁, w.not_measurable hj₁]