exact ⟨_, hx⟩
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : CS n E
R x✝ v x : ℝ
hx : ∀ (y : ℝ), ((fun a => ‖a‖) ∘ f.toFun) y ≤ ((fun a => ‖a‖) ∘ f.toFun) x
⊢ ∃ C, ∀ (v : ℝ), ‖f.toFun v‖ ≤ C
no goals