Commit 2022-03-30 13:52 e31f0319

feat(analysis/locally_convex): polar sets for dualities (#12849) Define the absolute polar for a duality and prove easy properties such as

• linear_map.polar_eq_Inter: The polar as an intersection.
• linear_map.subset_bipolar: The polar is a subset of the bipolar.
• linear_map.polar_weak_closed: The polar is closed in the weak topology induced by B.flip. Moreover, the corresponding lemmas are removed in the normed space setting as they all follow directly from the general case.