mathlib

4bf7ae47 - refactor(analysis/normed_space): use `lt` in rescale_to_shell, DRY (#4969)

refactor(analysis/normed_space): use `lt` in rescale_to_shell, DRY (#4969) * Use strict inequality for the upper bound in `rescale_to_shell`. * Deduplicate some proofs about operator norm. * Add `linear_map.bound_of_shell`, `continuous_linear_map.op_norm_le_of_shell`, and `continuous_linear_map.op_norm_le_of_shell'`.