Bounding the operator norm of a CLM on a dense set

Stream: Is there code for X?

[Moritz Doll]

Hey,
I am trying to find some version of the following statement: let f : E -> Fbe a CLM between normed spaces and s : Set E be dense. If forall x : s, we have that $\|f x\| \leq C \|x\|$, then $\|f\| \leq C.$ I don't see anything related, so any pointers would be welcome.

[Anatole Dedecker]

I don't recall seeing such a theorem. The proof should be essentially immediate using docs#Dense.induction

[Moritz Doll]

Perfect, this is exactly what I was looking for.