case pos
α : Type u_1
β : Type ?u.581843
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
hi₁ : MeasurableSet i
⊢ 0 ≤ ↑v i

case neg
α : Type u_1
β : Type ?u.581843
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ ↑v i
α : Type u_1
β : Type ?u.581843
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
⊢ 0 ≤ ↑v i
by_cases hi₁ : MeasurableSet i
no goals
case pos
α : Type u_1
β : Type ?u.581843
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
hi₁ : MeasurableSet i
⊢ 0 ≤ ↑v i
exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl
no goals
case neg
α : Type u_1
β : Type ?u.581843
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ ↑v i
rw [v.not_measurable hi₁]