mathlib3

97417665 - feat(analysis/normed_space): normed space is homeomorphic to the unit ball (#10690)