mathlib3

c4f673cb - chore(analysis/normed_space/basic): `continuous_at.norm` etc (#5411)

chore(analysis/normed_space/basic): `continuous_at.norm` etc (#5411) Add variants of the lemma that the norm is continuous. Also rewrite a few proofs, and rename three lemmas: * `lim_norm` -> `tendsto_norm_sub_self` * `lim_norm_zero` -> `tendsto_norm_zero` * `lim_norm_zero'` -> `tendsto_norm_zero'` Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>