Commit 2019-11-24 10:11 2d54a70a

feat(analysis/normed_space): prove more lemmas, rename some old lemmas (#1733) Renamed lemmas:

• norm_triangle → norm_add_le
• norm_triangle_sub → norm_sub_le
• norm_triangle_sum → norm_sum_le
• norm_reverse_triangle' → norm_sub_norm_le
• norm_reverse_triangle: deleted; was a duplicate of abs_norm_sub_norm_le
• nnorm_triangle → nnorm_add_le New lemmas:
• dist_add_left, dist_add_right, dist_neg_neg, dist_sub_left, dist_sub_right, dist_smul, dist_add_add_le, dist_sub_sub_le: operate with distances without rewriting them as norms.
• norm_add_le_of_le, dist_add_add_le_of_le, dist_sub_sub_le_of_le, norm_sum_le_of_le : chain a triangle-like inequality with an appropriate estimates on the right hand side. Also simplify a few proofs and fix a typo in a comment.