feat: lemmas about betweeness on a linear space (leanprover-community#26555)

This PR also adds aliases of the inverse direction of betweeness iff lemmas.

Author: Komyyy

Mathlib/Analysis/Convex/Between.lean

@@ -188,45 +188,131 @@ theorem wbtw_const_vadd_iff {x y z : P} (v : V) :
     Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Wbtw R x y z :=
   mem_const_vadd_affineSegment _
 
+alias ⟨_, Wbtw.const_vadd⟩ := wbtw_const_vadd_iff
+
+@[simp]
+theorem wbtw_const_add_iff {x y z : V} (v : V) :
+    Wbtw R (v + x) (v + y) (v + z) ↔ Wbtw R x y z :=
+  wbtw_const_vadd_iff v
+
+alias ⟨_, Wbtw.const_add⟩ := wbtw_const_add_iff
+
 @[simp]
 theorem wbtw_vadd_const_iff {x y z : V} (p : P) :
     Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Wbtw R x y z :=
   mem_vadd_const_affineSegment _
 
+alias ⟨_, Wbtw.vadd_const⟩ := wbtw_vadd_const_iff
+
+@[simp]
+theorem wbtw_add_const_iff {x y z : V} (v : V) :
+    Wbtw R (x + v) (y + v) (z + v) ↔ Wbtw R x y z :=
+  wbtw_vadd_const_iff v
+
+alias ⟨_, Wbtw.add_const⟩ := wbtw_add_const_iff
+
 @[simp]
 theorem wbtw_const_vsub_iff {x y z : P} (p : P) :
     Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Wbtw R x y z :=
   mem_const_vsub_affineSegment _
 
+alias ⟨_, Wbtw.const_vsub⟩ := wbtw_const_vsub_iff
+
+@[simp]
+theorem wbtw_const_sub_iff {x y z : V} (v : V) :
+    Wbtw R (v - x) (v - y) (v - z) ↔ Wbtw R x y z :=
+  wbtw_const_vsub_iff v
+
+alias ⟨_, Wbtw.const_sub⟩ := wbtw_const_sub_iff
+
+@[simp]
+theorem wbtw_neg_iff {x y z : V} :
+    Wbtw R (-x) (-y) (-z) ↔ Wbtw R x y z := by
+  simp only [← zero_sub, wbtw_const_sub_iff]
+
+alias ⟨_, Wbtw.neg⟩ := wbtw_neg_iff
+
 @[simp]
 theorem wbtw_vsub_const_iff {x y z : P} (p : P) :
     Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Wbtw R x y z :=
   mem_vsub_const_affineSegment _
 
+alias ⟨_, Wbtw.vsub_const⟩ := wbtw_vsub_const_iff
+
+@[simp]
+theorem wbtw_sub_const_iff {x y z : V} (v : V) :
+    Wbtw R (x - v) (y - v) (z - v) ↔ Wbtw R x y z :=
+  wbtw_vsub_const_iff v
+
+alias ⟨_, Wbtw.sub_const⟩ := wbtw_sub_const_iff
+
 @[simp]
 theorem sbtw_const_vadd_iff {x y z : P} (v : V) :
     Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z := by
   rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
     (AddAction.injective v).ne_iff]
 
+alias ⟨_, Sbtw.const_vadd⟩ := sbtw_const_vadd_iff
+
+@[simp]
+theorem sbtw_const_add_iff {x y z : V} (v : V) :
+    Sbtw R (v + x) (v + y) (v + z) ↔ Sbtw R x y z :=
+  sbtw_const_vadd_iff v
+
+alias ⟨_, Sbtw.const_add⟩ := sbtw_const_add_iff
+
 @[simp]
 theorem sbtw_vadd_const_iff {x y z : V} (p : P) :
     Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z := by
   rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
     (vadd_right_injective p).ne_iff]
 
+alias ⟨_, Sbtw.vadd_const⟩ := sbtw_vadd_const_iff
+
+@[simp]
+theorem sbtw_add_const_iff {x y z : V} (v : V) :
+    Sbtw R (x + v) (y + v) (z + v) ↔ Sbtw R x y z :=
+  sbtw_vadd_const_iff v
+
+alias ⟨_, Sbtw.add_const⟩ := sbtw_add_const_iff
+
 @[simp]
 theorem sbtw_const_vsub_iff {x y z : P} (p : P) :
     Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z := by
   rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
     (vsub_right_injective p).ne_iff]
 
+alias ⟨_, Sbtw.const_vsub⟩ := sbtw_const_vsub_iff
+
+@[simp]
+theorem sbtw_const_sub_iff {x y z : V} (v : V) :
+    Sbtw R (v - x) (v - y) (v - z) ↔ Sbtw R x y z :=
+  sbtw_const_vsub_iff v
+
+alias ⟨_, Sbtw.const_sub⟩ := sbtw_const_sub_iff
+
+@[simp]
+theorem sbtw_neg_iff {x y z : V} :
+    Sbtw R (-x) (-y) (-z) ↔ Sbtw R x y z := by
+  simp only [← zero_sub, sbtw_const_sub_iff]
+
+alias ⟨_, Sbtw.neg⟩ := sbtw_neg_iff
+
 @[simp]
 theorem sbtw_vsub_const_iff {x y z : P} (p : P) :
     Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z := by
   rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff,
     (vsub_left_injective p).ne_iff]
 
+alias ⟨_, Sbtw.vsub_const⟩ := sbtw_vsub_const_iff
+
+@[simp]
+theorem sbtw_sub_const_iff {x y z : V} (v : V) :
+    Sbtw R (x - v) (y - v) (z - v) ↔ Sbtw R x y z :=
+  sbtw_vsub_const_iff v
+
+alias ⟨_, Sbtw.sub_const⟩ := sbtw_sub_const_iff
+
 theorem Sbtw.wbtw {x y z : P} (h : Sbtw R x y z) : Wbtw R x y z :=
   h.1