Commit 2020-11-11 13:39 4bf7ae47

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'.