Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes