Commit 2025-10-14 23:03 8a1a1e3f

View on Github →

refactor(Analysis/LocallyConvex/AbsConvex): Redefine AbsConvex to use a single ring of scalars (#29342) Currently the definition of Absolutely Convex in Mathlib is a little unexpected:

def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s

At the time this definition was formulated, Mathlib's definition of Convex required the scalars to be an OrderedSemiring whereas the definition of Balanced required the scalars to be a SeminormedRing. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as AbsConvex if it is balanced over a SeminormedRing 𝕜 and convex over ℝ. Recently the requirements for the definition of Convex have been relaxed (#24392, #20595) so it is now possible to use a single scalar ring in common with the literature. Previous discussion:

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

modified def AbsConvex

modified theorem absConvexHull_eq_convexHull_balancedHull

modified theorem convex_absConvexHull

modified theorem nhds_hasBasis_absConvex_open

modified theorem zero_mem_absConvexHull

Modified Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean

modified theorem AbsConvexOpenSets.coe_convex

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

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