α : Type u_4
β : Type ?u.1299864
E : Type u_2
F : Type u_3
inst✝⁷ : MeasurableSpace α
ι : Type ?u.1299876
inst✝⁶ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
L : E →L[𝕜] F
⊢ Continuous fun x => ∫ (a : α), ↑↑(compLp L x) a ∂μ
α : Type u_4
β : Type ?u.1299864
E : Type u_2
F : Type u_3
inst✝⁷ : MeasurableSpace α
ι : Type ?u.1299876
inst✝⁶ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
L : E →L[𝕜] F
⊢ Continuous fun φ => ∫ (a : α), ↑L (↑↑φ a) ∂μ
rw [← funext L.integral_compLp]
no goals
α : Type u_4
β : Type ?u.1299864
E : Type u_2
F : Type u_3
inst✝⁷ : MeasurableSpace α
ι : Type ?u.1299876
inst✝⁶ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
L : E →L[𝕜] F
⊢ Continuous fun x => ∫ (a : α), ↑↑(compLp L x) a ∂μ
exact continuous_integral.comp (L.compLpL 1 μ).continuous