α : Type u_3
β : Type ?u.635196
m : MeasurableSpace α
L : Type ?u.635202
M : Type u_2
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
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(r • v) s = 0
α : Type u_3
β : Type ?u.635196
m : MeasurableSpace α
L : Type ?u.635202
M : Type u_2
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
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ r • v ≪ᵥ w
intro s hs
no goals
α : Type u_3
β : Type ?u.635196
m : MeasurableSpace α
L : Type ?u.635202
M : Type u_2
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
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(r • v) s = 0
rw [smul_apply, h hs, smul_zero]