feat(analysis/normed_space/dual): add lemmas, golf (#11132)
* add `polar_univ`, `is_closed_polar`, `polar_gc`, `polar_Union`,
`polar_union`, `polar_antitone`, `polar_zero`, `polar_closure`;
* extract `polar_ball_subset_closed_ball_div` and
`closed_ball_inv_subset_polar_closed_ball` out of the proofs of
`polar_closed_ball` and `polar_bounded_of_nhds_zero`;
* rename `polar_bounded_of_nhds_zero` to
`bounded_polar_of_mem_nhds_zero`, use `metric.bounded`;
* use `r⁻¹` instead of `1 / r` in `polar_closed_ball`. This is the
simp normal form (though we might want to change this in the future).
