mathlib

3d948bf1 - feat(analysis/normed_space): interior of `closed_ball` etc (#2723)

feat(analysis/normed_space): interior of `closed_ball` etc (#2723) * define `sphere x r` * prove formulas for `interior`, `closure`, and `frontier` of open and closed balls in real normed vector spaces.