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