basic): spheres have no interior (#18869)

Commit

2 years ago

feat(analysis/normed_space/basic): spheres have no interior (#18869) This follows the pattern set by the nearby lemmas of having a primed and unprimed version.

Author

eric-wieser

Parents

f0b3759a

mathlib 8000bbbe - feat(analysis/normed_space/basic): spheres have no interior (#18869)

mathlib
8000bbbe - feat(analysis/normed_space/basic): spheres have no interior (#18869)