Commit 2026-06-30 22:07 1ce27967
View on Github →chore(Analysis/Convex/Gauge): rename lemmas involving {x | prop (gauge s x)} (#40710)
Lemmas in Mathlib.Analysis.Convex.Gauge whose conclusions are of the form {x | prop (gauge s x)} are renamed to include setOf_gauge in the name rather than just gauge in line with recent work related to minkowski's second theorem. Deprecation aliases are added for all non-private renames.
Two downstream callers (AbsConvexOpen.lean, Bernstein.lean) are updated to use the new names.
Also moved Balanced.starConvex further up the import chain.
AI Disclosure: Generated with claude code