mathlib3

357b2966 - feat(analysis/convex/side): betweenness and affine subspaces (#16733)

feat(analysis/convex/side): betweenness and affine subspaces (#16733) Define notions of points being (weakly or strictly) on the same side or opposite sides of an affine subspace (e.g. a line), for use in describing geometrical configurations, and provide some associated API.