Normed spaces over R or C #
This file is about results on normed spaces over the fields
Main definitions #
Main theorems #
ContinuousLinearMap.op_norm_bound_of_ball_bound: A bound on the norms of values of a linear map in a ball yields a bound on the operator norm.
This file exists mainly to avoid importing
IsROrC in the main normed space theory files.
LinearMap.bound_of_ball_bound is a version of this over arbitrary nontrivially normed fields.
It produces a less precise bound so we keep both versions.