case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f

case neg
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f
by_cases hf : Measurable f
case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : ↑(VectorMeasure.map w f) s = 0
⊢ ↑(VectorMeasure.map v f) s = 0
case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f
refine' mk fun s hs hws => _
case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : ↑w (f ⁻¹' s) = 0
⊢ ↑v (f ⁻¹' s) = 0
case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : ↑(VectorMeasure.map w f) s = 0
⊢ ↑(VectorMeasure.map v f) s = 0
rw [map_apply _ hf hs] at hws⊢
no goals
case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : ↑w (f ⁻¹' s) = 0
⊢ ↑v (f ⁻¹' s) = 0
exact h hws
case neg
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
a✝ : ↑(VectorMeasure.map w f) s = 0
⊢ ↑(VectorMeasure.map v f) s = 0
case neg
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f
intro s _
no goals
case neg
α : Type u_2
β : Type u_1
m : MeasurableSpace α
L : Type ?u.642970
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
a✝ : ↑(VectorMeasure.map w f) s = 0
⊢ ↑(VectorMeasure.map v f) s = 0
rw [map_not_measurable v hf, zero_apply]