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.