Commit 2025-03-31 14:24 5c8cf415

View on Github →

feat(Analysis/Convex/BetweenList): betweenness for lists of points (#22178) Define the notions of a list of points in an affine space being weakly or strictly in order on a line.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/BetweenList.lean

added theorem AffineEquiv.list_sbtw_map_iff

added theorem AffineEquiv.list_wbtw_map_iff

added theorem Function.Injective.list_sbtw_map_iff

added theorem Function.Injective.list_wbtw_map_iff

added theorem List.Sbtw.pairwise_ne

added theorem List.Sorted.sbtw

added theorem List.Sorted.wbtw

added theorem List.exists_map_eq_of_sorted_iff_sbtw

added theorem List.exists_map_eq_of_sorted_iff_wbtw

added theorem List.exists_map_eq_of_sorted_nonempty_iff_sbtw

added theorem List.exists_map_eq_of_sorted_nonempty_iff_wbtw

added theorem List.sbtw_cons

added theorem List.sbtw_four

added theorem List.sbtw_iff_triplewise_and_ne_pair

added theorem List.sbtw_nil

added theorem List.sbtw_pair

added theorem List.sbtw_singleton

added theorem List.sbtw_triple

added theorem List.wbtw_cons

added theorem List.wbtw_four

added theorem List.wbtw_nil

added theorem List.wbtw_pair

added theorem List.wbtw_singleton

added theorem List.wbtw_triple