Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-16 07:51 a452bfa1

View on Github →

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.

Estimated changes