mathlib3

54293c4c - feat(analysis/convex/between): spans and `Ici`, `Ioi` images (#17601)

feat(analysis/convex/between): spans and `Ici`, `Ioi` images (#17601) Add a series of lemmas relating betweenness to one point being in the affine span of the other two and the right or left point being in an appropriate image of `Ici` or `Ioi` for `line_map` on the other two points.