Commit 2021-10-24 08:26 416edeed
View on Github →feat(analysis/normed_space/is_R_or_C): add three lemmas on bounds of linear maps over is_R_or_C. (#9827)
Adding lemmas linear_map.bound_of_sphere_bound
, linear_map.bound_of_ball_bound
, continuous_linear_map.op_norm_bound_of_ball_bound
as a preparation of a PR on Banach-Alaoglu theorem.