α : Type u_2
β : Type ?u.630299
m : MeasurableSpace α
L : Type ?u.630305
M : Type u_1
N : Type u_3
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✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ + v₂) s = 0
α : Type u_2
β : Type ?u.630299
m : MeasurableSpace α
L : Type ?u.630305
M : Type u_1
N : Type u_3
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✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ + v₂ ≪ᵥ w
intro s hs
no goals
α : Type u_2
β : Type ?u.630299
m : MeasurableSpace α
L : Type ?u.630305
M : Type u_1
N : Type u_3
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✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ + v₂) s = 0
rw [add_apply, hv₁ hs, hv₂ hs, zero_add]