case pos
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ map 0 f = 0

case neg
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
⊢ map 0 f = 0
by_cases hf : Measurable f
case pos.h
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
⊢ MeasurableSet i → ↑(map 0 f) i = ↑0 i
case pos
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ map 0 f = 0
ext i
case pos.h
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map 0 f) i = ↑0 i
case pos.h
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
⊢ MeasurableSet i → ↑(map 0 f) i = ↑0 i
intro hi
no goals
case pos.h
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map 0 f) i = ↑0 i
rw [map_apply _ hf hi, zero_apply, zero_apply]
no goals
case neg
α : Type u_3
β : Type u_1
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0
exact dif_neg hf