α : Type u_1
β : Type ?u.622187
m : MeasurableSpace α
L : Type ?u.622193
M : Type u_3
N : Type u_2
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0
α : Type u_1
β : Type ?u.622187
m : MeasurableSpace α
L : Type ?u.622193
M : Type u_3
N : Type u_2
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
⊢ v ≪ᵥ w
intro s hs
case pos
α : Type u_1
β : Type ?u.622187
m : MeasurableSpace α
L : Type ?u.622193
M : Type u_3
N : Type u_2
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0

case neg
α : Type u_1
β : Type ?u.622187
m : MeasurableSpace α
L : Type ?u.622193
M : Type u_3
N : Type u_2
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0
α : Type u_1
β : Type ?u.622187
m : MeasurableSpace α
L : Type ?u.622193
M : Type u_3
N : Type u_2
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0
by_cases hmeas : MeasurableSet s
no goals
case pos
α : Type u_1
β : Type ?u.622187
m : MeasurableSpace α
L : Type ?u.622193
M : Type u_3
N : Type u_2
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0
exact h hmeas hs
no goals
case neg
α : Type u_1
β : Type ?u.622187
m : MeasurableSpace α
L : Type ?u.622193
M : Type u_3
N : Type u_2
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0
exact not_measurable v hmeas