Theorem: intervalIntegral.norm_integral_le_of_norm_le_const' (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : 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|
Tactic:
apply intervalIntegral.norm_integral_le_of_norm_le_const
State after:
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

State before:
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
Tactic:
exact fun x hx ↦ h x <| mem_Icc_of_Ioc <| uIoc_of_le hab ▸ hx
State after:
no goals