Commit 2025-04-08 03:56 a4ad2aaa

View on Github →

feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex (#21002) Show that the absolute polar is weak*-closed and absolutely convex. Via closedAbsConvexHull_min this establishes the easy direction of the Bipolar Theorem #20843

Estimated changes

Modified Mathlib/Analysis/Convex/Basic.lean

modified theorem Convex.is_linear_preimage

modified theorem Convex.linear_preimage

Modified Mathlib/Analysis/LocallyConvex/AbsConvex.lean

added theorem AbsConvex.iInter₂

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

added theorem Balanced.mulActionHom_preimage

Modified Mathlib/Analysis/Normed/Module/Dual.lean

added theorem LinearMap.polar_AbsConvex