mathlib

699c2cab - feat(analysis/convex/between): betweenness in affine spaces (#16191)

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.