mathlib3

d6c1cf16 - feat(analysis/normed_space/pointwise): Balls disjointness (#13379)

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.