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

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