∀ {V : Type u_2} {W : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W] (f : V →+ W)
  (C : NNReal), (∀ (x : V), ‖f x‖₊ ≤ C * ‖x‖₊) → ∃ C, ∀ (v : V), ‖(↑f).toFun v‖ ≤ C * ‖v‖