Betweenness for lists of points.

This file defines notions of lists of points in an affine space being in order on a line.

Main definitions

• List.Wbtw R l: The points in list l are weakly in order on a line.
• List.Sbtw R l: The points in list l are strictly in order on a line.

def List.Wbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (l : List P) : Prop

The points in a list are weakly in that order on a line.

theorem List.wbtw_cons {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] {p : P} {l : List P} : List.Wbtw R (p :: l) ↔ Pairwise (Wbtw R p) l ∧ List.Wbtw R l

def List.Sbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (l : List P) : Prop

The points in a list are strictly in that order on a line.

@[simp]

theorem List.wbtw_nil (R : Type u_1) {V : Type u_2} (P : Type u_4) [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] : List.Wbtw R []

@[simp]

theorem List.sbtw_nil (R : Type u_1) {V : Type u_2} (P : Type u_4) [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] : List.Sbtw R []

@[simp]

theorem List.wbtw_singleton (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) : List.Wbtw R [p₁]

@[simp]

theorem List.sbtw_singleton (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) : List.Sbtw R [p₁]

@[simp]

theorem List.wbtw_pair (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ p₂ : P) : List.Wbtw R [p₁, p₂]

@[simp]

theorem List.sbtw_pair (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] {p₁ p₂ : P} : List.Sbtw R [p₁, p₂] ↔ p₁ ≠ p₂

@[simp]

theorem List.wbtw_triple {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] {p₁ p₂ p₃ : P} : List.Wbtw R [p₁, p₂, p₃] ↔ Wbtw R p₁ p₂ p₃

@[simp]

theorem List.sbtw_triple {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [IsOrderedRing R] {p₁ p₂ p₃ : P} : List.Sbtw R [p₁, p₂, p₃] ↔ Sbtw R p₁ p₂ p₃

theorem List.wbtw_four {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] {p₁ p₂ p₃ p₄ : P} : List.Wbtw R [p₁, p₂, p₃, p₄] ↔ Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄ ∧ Wbtw R p₁ p₃ p₄ ∧ Wbtw R p₂ p₃ p₄

theorem List.sbtw_four {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [IsOrderedRing R] {p₁ p₂ p₃ p₄ : P} : List.Sbtw R [p₁, p₂, p₃, p₄] ↔ Sbtw R p₁ p₂ p₃ ∧ Sbtw R p₁ p₂ p₄ ∧ Sbtw R p₁ p₃ p₄ ∧ Sbtw R p₂ p₃ p₄

theorem List.Sbtw.wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] {l : List P} (h : List.Sbtw R l) : List.Wbtw R l

theorem List.Sbtw.pairwise_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] {l : List P} (h : List.Sbtw R l) : Pairwise (fun (x1 x2 : P) => x1 ≠ x2) l

theorem List.sbtw_iff_triplewise_and_ne_pair {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [IsOrderedRing R] {l : List P} : List.Sbtw R l ↔ Triplewise (Sbtw R) l ∧ ∀ (a : P), l ≠ [a, a]

theorem List.sbtw_cons {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [IsOrderedRing R] {p : P} {l : List P} : List.Sbtw R (p :: l) ↔ Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]

theorem List.Wbtw.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {l : List P} (h : List.Wbtw R l) (f : P →ᵃ[R] P') : List.Wbtw R (map (⇑f) l)

theorem Function.Injective.list_wbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {l : List P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : List.Wbtw R (List.map (⇑f) l) ↔ List.Wbtw R l

theorem Function.Injective.list_sbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {l : List P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : List.Sbtw R (List.map (⇑f) l) ↔ List.Sbtw R l

theorem AffineEquiv.list_wbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {l : List P} (f : P ≃ᵃ[R] P') : List.Wbtw R (List.map (⇑f) l) ↔ List.Wbtw R l

theorem AffineEquiv.list_sbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {l : List P} (f : P ≃ᵃ[R] P') : List.Sbtw R (List.map (⇑f) l) ↔ List.Sbtw R l

theorem List.Sorted.wbtw {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {l : List R} (h : Sorted (fun (x1 x2 : R) => x1 ≤ x2) l) : List.Wbtw R l

theorem List.Sorted.sbtw {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {l : List R} (h : Sorted (fun (x1 x2 : R) => x1 < x2) l) : List.Sbtw R l

theorem List.exists_map_eq_of_sorted_nonempty_iff_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {l : List P} (hl : l ≠ []) : (∃ (l' : List R), Sorted (fun (x1 x2 : R) => x1 ≤ x2) l' ∧ map (⇑(AffineMap.lineMap (l.head hl) (l.getLast hl))) l' = l) ↔ List.Wbtw R l

theorem List.exists_map_eq_of_sorted_iff_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {l : List P} : (∃ (p₁ : P) (p₂ : P) (l' : List R), Sorted (fun (x1 x2 : R) => x1 ≤ x2) l' ∧ map (⇑(AffineMap.lineMap p₁ p₂)) l' = l) ↔ List.Wbtw R l

theorem List.exists_map_eq_of_sorted_nonempty_iff_sbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {l : List P} (hl : l ≠ []) : (∃ (l' : List R), Sorted (fun (x1 x2 : R) => x1 < x2) l' ∧ map (⇑(AffineMap.lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) ↔ List.Sbtw R l

theorem List.exists_map_eq_of_sorted_iff_sbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Nontrivial P] {l : List P} : (∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), Sorted (fun (x1 x2 : R) => x1 < x2) l' ∧ map (⇑(AffineMap.lineMap p₁ p₂)) l' = l) ↔ List.Sbtw R l