Mathlib Changelog
v4
Changelog
About
Github
Theorem
StrictConvex.extremePoints_eq_diff_interior
Modification history
2026-03-10 19:38
Mathlib/Analysis/Convex/Strict/Extreme.lean
feat(Analysis/Convex): `extremePoints ℝ (closedBall x r) ⊆ sphere x r` (#35899) …
Added
StrictConvex.extremePoints_eq_diff_interior
View on Github →