Commit 2022-09-30 13:10 699c2cab

feat(analysis/convex/between): betweenness in affine spaces (#16191) Define the notions of (weak and strict) betweenness for points in affine spaces over an ordered ring, for use in describing geometrical configurations. Until convexity is refactored to support abstract affine combination spaces, this means having a definition affine_segment that duplicates segment in the affine space case (and is proved to equal segment when the affine space is a module considered as an affine space over itself). However, the bulk of results concern betweenness, not affine_segment, and so would be just as relevant after such a refactor, even if some of the proofs would change, and indeed most of the things stated about affine_segment involve +ᵥ and -ᵥ and so would still be meaningful results, distinct from those already present for segment, after such a refactor (at which point they might apply for whatever typeclass describes an add_torsor for a module that is also an abstract affine combination space where the two affine combination structures agree). So I think the actual duplication here is minimal and defining affine_segment is a reasonable approach to allow betweenness to be handled in affine spaces now rather than making it depend on a possible future refactor. There are certainly more things that could sensibly be stated about betweenness (e.g. various forms of Pasch's axiom), but I think this is a reasonable starting point. One thing I definitely intend to add in a followup is notions of two points being (weakly or strictly) on the same side or opposite sides of an affine subspace (e.g. a line); I think it will probably be most convenient to define those notions in terms of same_ray and then prove appropriate results about how they relate to betweenness for points.