Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-19 03:39 190dd106

View on Github →

chore(analysis/normed_space): golf some proofs (#5804)

  • add pi_norm_lt_iff;
  • add has_sum.norm_le_of_bounded;
  • add multilinear_map.bound_of_shell;
  • rename continuous_multilinear_map.norm_image_sub_le_of_bound to continuous_multilinear_map.norm_image_sub_le, same with prime version;
  • golf some proofs.

Estimated changes

added theorem pi_norm_lt_iff