mathlib

e1730698 - feat(analysis/convex/strict_convex_between): betweenness and strictly convex spaces (#17528)

feat(analysis/convex/strict_convex_between): betweenness and strictly convex spaces (#17528) Add some lemmas about betweenness in affine spaces for strictly convex spaces. Geometrically these are facts like "a point strictly between two points on or inside a sphere lies inside that sphere" (but since they don't depend on anything more than strict convexity, they're proved in that context rather than just a Euclidean context; appropriate Euclidean results will be deduced from these).