mathlib

a452bfa1 - feat(analysis/seminorm): three simple lemmas about balls (#12720)

feat(analysis/seminorm): three simple lemmas about balls (#12720) The lemmas are in preparation to characterize the natural bornology in terms of seminorms in LCTVSs.