basic): use weaker assumptions (#12260)

Commit

3 years ago

feat(analysis/normed_space/basic): use weaker assumptions (#12260) Assume `r ≠ 0` instead of `0 < r` in `interior_closed_ball` and `frontier_closed_ball`.

Author

urkud

Parents

620af85a

mathlib3 890338d4 - feat(analysis/normed_space/basic): use weaker assumptions (#12260)

mathlib3
890338d4 - feat(analysis/normed_space/basic): use weaker assumptions (#12260)