Commit 2025-05-03 23:07 22711cf7

View on Github →

feat: special case of Disjoint.exists_open_convexes for a closed set and a singleton (#24259)

Estimated changes

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

modified theorem Disjoint.exists_open_convexes

added theorem exists_open_convex_of_not_mem