α : Type u_1
E : Type ?u.2308880
F : Type u_2
G : Type ?u.2308886
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ✝ ν✝ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
μ ν : Measure α
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂μ + ν) = (∫⁻ (x : α), ↑‖f x‖₊ ∂μ) + ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
α : Type u_1
E : Type ?u.2308880
F : Type u_2
G : Type ?u.2308886
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ✝ ν✝ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
μ ν : Measure α
⊢ snorm f 1 (μ + ν) = snorm f 1 μ + snorm f 1 ν
simp_rw [snorm_one_eq_lintegral_nnnorm]
no goals
α : Type u_1
E : Type ?u.2308880
F : Type u_2
G : Type ?u.2308886
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ✝ ν✝ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
μ ν : Measure α
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂μ + ν) = (∫⁻ (x : α), ↑‖f x‖₊ ∂μ) + ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
rw [lintegral_add_measure _ μ ν]