Commit 2021-12-30 00:20 ea95523d

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).