α : Type u_1
β : Type ?u.540108
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
⊢ ↑v i ≤ ↑w i
α : Type u_1
β : Type ?u.540108
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
⊢ v ≤ w ↔ ∀ (i : Set α), ↑v i ≤ ↑w i
refine' ⟨fun h i => _, fun h i _ => h i⟩
case pos
α : Type u_1
β : Type ?u.540108
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : MeasurableSet i
⊢ ↑v i ≤ ↑w i

case neg
α : Type u_1
β : Type ?u.540108
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i ≤ ↑w i
α : Type u_1
β : Type ?u.540108
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
⊢ ↑v i ≤ ↑w i
by_cases hi : MeasurableSet i
no goals
case pos
α : Type u_1
β : Type ?u.540108
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : MeasurableSet i
⊢ ↑v i ≤ ↑w i
exact h i hi
no goals
case neg
α : Type u_1
β : Type ?u.540108
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i ≤ ↑w i
rw [v.not_measurable hi, w.not_measurable hi]