Commit 2026-05-21 09:56 63ad6315

feat(Geometry/Convex): convex sets in a ConvexSpace (#38905) Define convex sets in a convex space. To allow full generality on the coefficients, for s to be convex we require that all finitary convex combinations of points of s lie in s, instead of merely binary ones as is customary. Since its body is an implementation detail, the predicate IsConvexSet is unexposed. Convex will be deprecated to IsConvexSet in a later PR. Zulip