case h
α : Type u_1
β : Type ?u.336628
m inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange (v + w) f hf) i✝ = ↑(mapRange v f hf + mapRange w f hf) i✝
α : Type u_1
β : Type ?u.336628
m inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
⊢ mapRange (v + w) f hf = mapRange v f hf + mapRange w f hf
ext
no goals
case h
α : Type u_1
β : Type ?u.336628
m inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange (v + w) f hf) i✝ = ↑(mapRange v f hf + mapRange w f hf) i✝
simp