Commit 2024-09-19 04:26 c16a940a

View on Github →

feat: closures of convex sets in locally convex spaces with the same continuous linear functionals (#16859)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/WeakSpace.lean

added theorem Convex.toWeakSpace_closure

added theorem LinearEquiv.image_closure_of_convex'

added theorem LinearEquiv.image_closure_of_convex

added theorem LinearMap.image_closure_of_convex

Modified Mathlib/Topology/Algebra/Module/WeakBilin.lean

Modified Mathlib/Topology/Algebra/Module/WeakDual.lean

deleted def continuousLinearMapToWeakSpace

deleted theorem continuousLinearMapToWeakSpace_bijective

deleted theorem continuousLinearMapToWeakSpace_eq_toWeakSpace

added def toWeakSpaceCLM

added theorem toWeakSpaceCLM_bijective

added theorem toWeakSpaceCLM_eq_toWeakSpace

modified theorem topDualPairing_apply