case mp
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ restrict v Set.univ ≤ restrict w Set.univ → v ≤ w

case mpr
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w → restrict v Set.univ ≤ restrict w Set.univ
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ restrict v Set.univ ≤ restrict w Set.univ ↔ v ≤ w
constructor
case mp
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : restrict v Set.univ ≤ restrict w Set.univ
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s
case mp
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ restrict v Set.univ ≤ restrict w Set.univ → v ≤ w
intro h s hs
case mp
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : restrict v Set.univ ≤ restrict w Set.univ
s : Set α
hs : MeasurableSet s
this : ↑(restrict v Set.univ) s ≤ ↑(restrict w Set.univ) s
⊢ ↑v s ≤ ↑w s
case mp
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : restrict v Set.univ ≤ restrict w Set.univ
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s
have := h s hs
no goals
case mp
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : restrict v Set.univ ≤ restrict w Set.univ
s : Set α
hs : MeasurableSet s
this : ↑(restrict v Set.univ) s ≤ ↑(restrict w Set.univ) s
⊢ ↑v s ≤ ↑w s
rwa [restrict_apply _ MeasurableSet.univ hs, Set.inter_univ,
  restrict_apply _ MeasurableSet.univ hs, Set.inter_univ] at this
case mpr
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑(restrict v Set.univ) s ≤ ↑(restrict w Set.univ) s
case mpr
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w → restrict v Set.univ ≤ restrict w Set.univ
intro h s hs
case mpr
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s
case mpr
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑(restrict v Set.univ) s ≤ ↑(restrict w Set.univ) s
rw [restrict_apply _ MeasurableSet.univ hs, Set.inter_univ,
  restrict_apply _ MeasurableSet.univ hs, Set.inter_univ]
no goals
case mpr
α : Type u_1
β : Type ?u.546843
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s
exact h s hs