α : Type u_1
E : Type u_2
F : Type ?u.449573
𝕜 : Type ?u.449576
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f g : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM (f + g) = ↑integralCLM f + ↑integralCLM g
α : Type u_1
E : Type u_2
F : Type ?u.449573
𝕜 : Type ?u.449576
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f g : { x // x ∈ Lp E 1 }
⊢ integral (f + g) = integral f + integral g
simp only [integral]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.449573
𝕜 : Type ?u.449576
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f g : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM (f + g) = ↑integralCLM f + ↑integralCLM g
exact map_add integralCLM f g