feat(analysis/normed_space): generalize some lemmas (#12959)
* add `metric.closed_ball_zero'`, a version of `metric.closed_ball_zero` for a pseudo metric space;
* merge `metric.closed_ball_inf_dist_compl_subset_closure'` with `metric.closed_ball_inf_dist_compl_subset_closure`, drop an unneeded assumption `s ≠ univ`;
* assume `r ≠ 0` instead of `0 < r` in `closure_ball`, `frontier_ball`, and `euclidean.closure_ball`.
