Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-15 15:03 d6c1cf16

View on Github →

feat(analysis/normed_space/pointwise): Balls disjointness (#13379) Two balls in a real normed space are disjoint iff the sum of their radii is less than the distance between their centers.

Estimated changes