case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.7355959
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Fact (1 ≤ p)
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ ↑(compLpL p μ (L + L')) f = ↑(compLpL p μ L + compLpL p μ L') f
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.7355959
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Fact (1 ≤ p)
L L' : E →L[𝕜] F
⊢ compLpL p μ (L + L') = compLpL p μ L + compLpL p μ L'
ext1 f
no goals
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.7355959
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Fact (1 ≤ p)
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ ↑(compLpL p μ (L + L')) f = ↑(compLpL p μ L + compLpL p μ L') f
exact add_compLp L L' f