α : Type u_1
β : Type ?u.604160
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬restrict v i ≤ restrict 0 i
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
α : Type u_1
β : Type ?u.604160
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬restrict v i ≤ restrict 0 i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
have hi₁ : MeasurableSet i := measurable_of_not_restrict_le_zero _ hi
α : Type u_1
β : Type ?u.604160
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑0 j
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
α : Type u_1
β : Type ?u.604160
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬restrict v i ≤ restrict 0 i
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
rw [restrict_le_restrict_iff _ _ hi₁] at hi
α : Type u_1
β : Type ?u.604160
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi : Exists fun ⦃j⦄ => MeasurableSet j ∧ j ⊆ i ∧ ↑0 j < ↑v j
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
α : Type u_1
β : Type ?u.604160
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑0 j
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
push_neg at hi
no goals
α : Type u_1
β : Type ?u.604160
m : MeasurableSpace α
M : Type u_2
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi : Exists fun ⦃j⦄ => MeasurableSet j ∧ j ⊆ i ∧ ↑0 j < ↑v j
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
exact hi