mathlib3

4a4c2753 - feat(analysis/normed_space/linear_isometry): add defs and lemmas (#15650)

feat(analysis/normed_space/linear_isometry): add defs and lemmas (#15650) * add `linear_isometry_equiv.of_top` and `linear_isometry.equiv_range`; * add lemmas about (pre)images of balls and spheres.