mathlib3
812e17f8 - feat(analysis/normed_space/pointwise): Addition of balls (#13381)

Commit
3 years ago
feat(analysis/normed_space/pointwise): Addition of balls (#13381) Adding two balls yields another ball.
Author
Parents
Loading