apply intervalIntegral.norm_integral_le_of_norm_le_const
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
a b C : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hab : a ≤ b
h : ∀ x ∈ Icc a b, ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
case h
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
a b C : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hab : a ≤ b
h : ∀ x ∈ Icc a b, ‖f x‖ ≤ C
⊢ ∀ x ∈ Ι a b, ‖f x‖ ≤ C