Commit 2022-02-24 00:25 890338d4
View on Github →feat(analysis/normed_space/basic): use weaker assumptions (#12260)
Assume r ≠ 0 instead of 0 < r in interior_closed_ball and frontier_closed_ball.
feat(analysis/normed_space/basic): use weaker assumptions (#12260)
Assume r ≠ 0 instead of 0 < r in interior_closed_ball and frontier_closed_ball.