case mp
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
⊢ v ≪ᵥ μ

case mpr
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
⊢ ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
⊢ (∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0) ↔ v ≪ᵥ μ
constructor <;> intro h
case mp
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
s : Set α
hmeas : MeasurableSet s
hs : ↑μ s = 0
⊢ ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
case mp
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
⊢ v ≪ᵥ μ
refine' mk fun s hmeas hs => h _
no goals
case mp
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
s : Set α
hmeas : MeasurableSet s
hs : ↑μ s = 0
⊢ ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
rw [← hs, ennrealToMeasure_apply hmeas]
case mpr
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
⊢ ↑v s = 0
case mpr
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
⊢ ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
intro s hs
case pos
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0

case neg
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0
case mpr
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
⊢ ↑v s = 0
by_cases hmeas : MeasurableSet s
case pos
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑μ s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0
case pos
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0
rw [ennrealToMeasure_apply hmeas] at hs
no goals
case pos
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑μ s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0
exact h hs
no goals
case neg
α : Type u_1
β : Type ?u.644845
m : MeasurableSpace α
L : Type ?u.644851
M : Type u_2
N : Type ?u.644857
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0
exact not_measurable v hmeas