Commit 2025-08-14 15:16 0d05dabb

View on Github →

feat: convex hull of s is a singleton iff s is a singleton (#28154) Also fix the misnamed convexHull_empty_iff. From MiscYD

Estimated changes

Modified Mathlib/Analysis/Convex/Hull.lean

deleted theorem convexHull_empty_iff

added theorem convexHull_eq_empty

added theorem convexHull_eq_singleton

added theorem convexHull_eq_zero