Normed spaces over R or C #
This file is about results on normed spaces over the fields
Main definitions #
Main theorems #
continuous_linear_map.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
is_R_or_C in the main normed space theory files.