case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ ↑↑(compLp (L + L') f) =ᵐ[μ] ↑↑(compLp L f + compLp L' f)
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ compLp (L + L') f = compLp L f + compLp L' f
ext1
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ (fun a => ↑(L + L') (↑↑f a)) =ᵐ[μ] ↑↑(compLp L f + compLp L' f)
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ ↑↑(compLp (L + L') f) =ᵐ[μ] ↑↑(compLp L f + compLp L' f)
refine' (coeFn_compLp' (L + L') f).trans _
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ (fun a => ↑(L + L') (↑↑f a)) =ᵐ[μ] ↑↑(compLp L f) + ↑↑(compLp L' f)
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ (fun a => ↑(L + L') (↑↑f a)) =ᵐ[μ] ↑↑(compLp L f + compLp L' f)
refine' EventuallyEq.trans _ (Lp.coeFn_add _ _).symm
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ (fun a => ↑(L + L') (↑↑f a)) =ᵐ[μ] fun x => ↑L (↑↑f x) + ↑L' (↑↑f x)
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ (fun a => ↑(L + L') (↑↑f a)) =ᵐ[μ] ↑↑(compLp L f) + ↑↑(compLp L' f)
refine'
  EventuallyEq.trans _ (EventuallyEq.add (L.coeFn_compLp' f).symm (L'.coeFn_compLp' f).symm)
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
x : α
⊢ (fun a => ↑(L + L') (↑↑f a)) x = (fun x => ↑L (↑↑f x) + ↑L' (↑↑f x)) x
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ (fun a => ↑(L + L') (↑↑f a)) =ᵐ[μ] fun x => ↑L (↑↑f x) + ↑L' (↑↑f x)
refine' eventually_of_forall fun x => _
no goals
case h
α : Type u_4
E : Type u_2
F : Type u_3
G : Type ?u.5467217
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
L L' : E →L[𝕜] F
f : { x // x ∈ Lp E p }
x : α
⊢ (fun a => ↑(L + L') (↑↑f a)) x = (fun x => ↑L (↑↑f x) + ↑L' (↑↑f x)) x
rfl