ι : Type ?u.11937590
𝕜 : Type ?u.11937593
E : Type u_1
F : Type ?u.11937599
A : Type ?u.11937602
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ ‖∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ‖
ι : Type ?u.11937590
𝕜 : Type ?u.11937593
E : Type u_1
F : Type ?u.11937599
A : Type ?u.11937602
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
⊢ ‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ abs (∫ (x : ℝ) in a..b, ‖f x‖ ∂μ)
simp only [← Real.norm_eq_abs, norm_integral_eq_norm_integral_Ioc]
no goals
ι : Type ?u.11937590
𝕜 : Type ?u.11937593
E : Type u_1
F : Type ?u.11937599
A : Type ?u.11937602
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ ‖∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ‖
exact le_trans (norm_integral_le_integral_norm _) (le_abs_self _)