# Betweenness in affine spaces #

This file defines notions of a point in an affine space being between two given points.

## Main definitions #

• affineSegment R x y: The segment of points weakly between x and y.
• Wbtw R x y z: The point y is weakly between x and z.
• Sbtw R x y z: The point y is strictly between x and z.
def affineSegment (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
Set P

The segment of points weakly between x and y. When convexity is refactored to support abstract affine combination spaces, this will no longer need to be a separate definition from segment. However, lemmas involving +ᵥ or -ᵥ will still be relevant after such a refactoring, as distinct from versions involving + or - in a module.

Equations
Instances For
theorem affineSegment_eq_segment (R : Type u_1) {V : Type u_2} [] [] [Module R V] (x : V) (y : V) :
= segment R x y
theorem affineSegment_comm (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
=
theorem left_mem_affineSegment (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
x
theorem right_mem_affineSegment (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
y
@[simp]
theorem affineSegment_same (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) :
= {x}
@[simp]
theorem affineSegment_image {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [] [] [Module R V] [] [] [Module R V'] [AddTorsor V' P'] (f : P →ᵃ[R] P') (x : P) (y : P) :
f '' = affineSegment R (f x) (f y)
@[simp]
theorem affineSegment_const_vadd_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) (v : V) :
(fun (x : P) => v +ᵥ x) '' = affineSegment R (v +ᵥ x) (v +ᵥ y)
@[simp]
theorem affineSegment_vadd_const_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : V) (y : V) (p : P) :
(fun (x : V) => x +ᵥ p) '' = affineSegment R (x +ᵥ p) (y +ᵥ p)
@[simp]
theorem affineSegment_const_vsub_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) (p : P) :
(fun (x : P) => p -ᵥ x) '' = affineSegment R (p -ᵥ x) (p -ᵥ y)
@[simp]
theorem affineSegment_vsub_const_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) (p : P) :
(fun (x : P) => x -ᵥ p) '' = affineSegment R (x -ᵥ p) (y -ᵥ p)
@[simp]
theorem mem_const_vadd_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (v : V) :
v +ᵥ z affineSegment R (v +ᵥ x) (v +ᵥ y) z
@[simp]
theorem mem_vadd_const_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : V} {y : V} {z : V} (p : P) :
z +ᵥ p affineSegment R (x +ᵥ p) (y +ᵥ p) z
@[simp]
theorem mem_const_vsub_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (p : P) :
p -ᵥ z affineSegment R (p -ᵥ x) (p -ᵥ y) z
@[simp]
theorem mem_vsub_const_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (p : P) :
z -ᵥ p affineSegment R (x -ᵥ p) (y -ᵥ p) z
def Wbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) (z : P) :

The point y is weakly between x and z.

Equations
Instances For
def Sbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) (z : P) :

The point y is strictly between x and z.

Equations
Instances For
theorem mem_segment_iff_wbtw {R : Type u_1} {V : Type u_2} [] [] [Module R V] {x : V} {y : V} {z : V} :
y segment R x z Wbtw R x y z
theorem Wbtw.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [] [] [Module R V] [] [] [Module R V'] [AddTorsor V' P'] {x : P} {y : P} {z : P} (h : Wbtw R x y z) (f : P →ᵃ[R] P') :
Wbtw R (f x) (f y) (f z)
theorem Function.Injective.wbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [] [] [Module R V] [] [] [Module R V'] [AddTorsor V' P'] {x : P} {y : P} {z : P} {f : P →ᵃ[R] P'} (hf : ) :
Wbtw R (f x) (f y) (f z) Wbtw R x y z
theorem Function.Injective.sbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [] [] [Module R V] [] [] [Module R V'] [AddTorsor V' P'] {x : P} {y : P} {z : P} {f : P →ᵃ[R] P'} (hf : ) :
Sbtw R (f x) (f y) (f z) Sbtw R x y z
@[simp]
theorem AffineEquiv.wbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [] [] [Module R V] [] [] [Module R V'] [AddTorsor V' P'] {x : P} {y : P} {z : P} (f : P ≃ᵃ[R] P') :
Wbtw R (f x) (f y) (f z) Wbtw R x y z
@[simp]
theorem AffineEquiv.sbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [] [] [Module R V] [] [] [Module R V'] [AddTorsor V' P'] {x : P} {y : P} {z : P} (f : P ≃ᵃ[R] P') :
Sbtw R (f x) (f y) (f z) Sbtw R x y z
@[simp]
theorem wbtw_const_vadd_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (v : V) :
Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) Wbtw R x y z
@[simp]
theorem wbtw_vadd_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : V} {y : V} {z : V} (p : P) :
Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) Wbtw R x y z
@[simp]
theorem wbtw_const_vsub_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (p : P) :
Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) Wbtw R x y z
@[simp]
theorem wbtw_vsub_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (p : P) :
Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) Wbtw R x y z
@[simp]
theorem sbtw_const_vadd_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (v : V) :
Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) Sbtw R x y z
@[simp]
theorem sbtw_vadd_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : V} {y : V} {z : V} (p : P) :
Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) Sbtw R x y z
@[simp]
theorem sbtw_const_vsub_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (p : P) :
Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) Sbtw R x y z
@[simp]
theorem sbtw_vsub_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (p : P) :
Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) Sbtw R x y z
theorem Sbtw.wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
Wbtw R x y z
theorem Sbtw.ne_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
y x
theorem Sbtw.left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
x y
theorem Sbtw.ne_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
y z
theorem Sbtw.right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
z y
theorem Sbtw.mem_image_Ioo {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
y () '' Set.Ioo 0 1
theorem Wbtw.mem_affineSpan {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
y affineSpan R {x, z}
theorem wbtw_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} :
Wbtw R x y z Wbtw R z y x
theorem Wbtw.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} :
Wbtw R x y zWbtw R z y x

Alias of the forward direction of wbtw_comm.

theorem sbtw_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} :
Sbtw R x y z Sbtw R z y x
theorem Sbtw.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} :
Sbtw R x y zSbtw R z y x

Alias of the forward direction of sbtw_comm.

@[simp]
theorem wbtw_self_left (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
Wbtw R x x y
@[simp]
theorem wbtw_self_right (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
Wbtw R x y y
@[simp]
theorem wbtw_self_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} :
Wbtw R x y x y = x
@[simp]
theorem not_sbtw_self_left (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
¬Sbtw R x x y
@[simp]
theorem not_sbtw_self_right (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
¬Sbtw R x y y
theorem Wbtw.left_ne_right_of_ne_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hne : y x) :
x z
theorem Wbtw.left_ne_right_of_ne_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hne : y z) :
x z
theorem Sbtw.left_ne_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
x z
theorem sbtw_iff_mem_image_Ioo_and_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {z : P} :
Sbtw R x y z y () '' Set.Ioo 0 1 x z
@[simp]
theorem not_sbtw_self (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] (x : P) (y : P) :
¬Sbtw R x y x
theorem wbtw_swap_left_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} (z : P) :
Wbtw R x y z Wbtw R y x z x = y
theorem wbtw_swap_right_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] (x : P) {y : P} {z : P} :
Wbtw R x y z Wbtw R x z y y = z
theorem wbtw_rotate_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] (x : P) {y : P} {z : P} :
Wbtw R x y z Wbtw R z x y x = y
theorem Wbtw.swap_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
Wbtw R y x z x = y
theorem Wbtw.swap_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
Wbtw R x z y y = z
theorem Wbtw.rotate_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
Wbtw R z x y x = y
theorem Sbtw.not_swap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
¬Wbtw R y x z
theorem Sbtw.not_swap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
¬Wbtw R x z y
theorem Sbtw.not_rotate {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
¬Wbtw R z x y
@[simp]
theorem wbtw_lineMap_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {r : R} :
Wbtw R x (() r) y x = y r Set.Icc 0 1
@[simp]
theorem sbtw_lineMap_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {x : P} {y : P} {r : R} :
Sbtw R x (() r) y x y r Set.Ioo 0 1
@[simp]
theorem wbtw_mul_sub_add_iff {R : Type u_1} [] [] {x : R} {y : R} {r : R} :
Wbtw R x (r * (y - x) + x) y x = y r Set.Icc 0 1
@[simp]
theorem sbtw_mul_sub_add_iff {R : Type u_1} [] [] {x : R} {y : R} {r : R} :
Sbtw R x (r * (y - x) + x) y x y r Set.Ioo 0 1
@[simp]
theorem wbtw_zero_one_iff {R : Type u_1} [] {x : R} :
Wbtw R 0 x 1 x Set.Icc 0 1
@[simp]
theorem wbtw_one_zero_iff {R : Type u_1} [] {x : R} :
Wbtw R 1 x 0 x Set.Icc 0 1
@[simp]
theorem sbtw_zero_one_iff {R : Type u_1} [] {x : R} :
Sbtw R 0 x 1 x Set.Ioo 0 1
@[simp]
theorem sbtw_one_zero_iff {R : Type u_1} [] {x : R} :
Sbtw R 1 x 0 x Set.Ioo 0 1
theorem Wbtw.trans_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) :
Wbtw R w x z
theorem Wbtw.trans_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w x z) (h₂ : Wbtw R x y z) :
Wbtw R w y z
theorem Wbtw.trans_sbtw_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w y z) (h₂ : Sbtw R w x y) :
Sbtw R w x z
theorem Wbtw.trans_sbtw_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w x z) (h₂ : Sbtw R x y z) :
Sbtw R w y z
theorem Sbtw.trans_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Sbtw R w y z) (h₂ : Sbtw R w x y) :
Sbtw R w x z
theorem Sbtw.trans_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Sbtw R w x z) (h₂ : Sbtw R x y z) :
Sbtw R w y z
theorem Wbtw.trans_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) (h : y z) :
x z
theorem Wbtw.trans_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w x z) (h₂ : Wbtw R x y z) (h : w x) :
w y
theorem Sbtw.trans_wbtw_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Sbtw R w y z) (h₂ : Wbtw R w x y) :
x z
theorem Sbtw.trans_wbtw_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Sbtw R w x z) (h₂ : Wbtw R x y z) :
w y
theorem Sbtw.affineCombination_of_mem_affineSpan_pair {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [] [Module R V] [] [] [] {ι : Type u_6} {p : ιP} (ha : ) {w : ιR} {w₁ : ιR} {w₂ : ιR} {s : } (hw : (s.sum fun (i : ι) => w i) = 1) (hw₁ : (s.sum fun (i : ι) => w₁ i) = 1) (hw₂ : (s.sum fun (i : ι) => w₂ i) = 1) (h : () w affineSpan R {() w₁, () w₂}) {i : ι} (his : i s) (hs : Sbtw R (w₁ i) (w i) (w₂ i)) :
Sbtw R (() w₁) (() w) (() w₂)
theorem Wbtw.sameRay_vsub {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
SameRay R (y -ᵥ x) (z -ᵥ y)
theorem Wbtw.sameRay_vsub_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
SameRay R (y -ᵥ x) (z -ᵥ x)
theorem Wbtw.sameRay_vsub_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
SameRay R (z -ᵥ x) (z -ᵥ y)
theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] [] {t : } {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ i₂) {p₁ : P} {p₂ : P} {p : P} (h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)) (h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)) (h₁' : p affineSpan R {t.points i₁, p₁}) (h₂' : p affineSpan R {t.points i₂, p₂}) :
Sbtw R (t.points i₁) p p₁

Suppose lines from two vertices of a triangle to interior points of the opposite side meet at p. Then p lies in the interior of the first (and by symmetry the other) segment from a vertex to the point on the opposite side.

theorem wbtw_iff_left_eq_or_right_mem_image_Ici {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} :
Wbtw R x y z x = y z () ''
theorem Wbtw.right_mem_image_Ici_of_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hne : x y) :
z () ''
theorem Wbtw.right_mem_affineSpan_of_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hne : x y) :
z affineSpan R {x, y}
theorem sbtw_iff_left_ne_and_right_mem_image_Ioi {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} :
Sbtw R x y z x y z () ''
theorem Sbtw.right_mem_image_Ioi {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
z () ''
theorem Sbtw.right_mem_affineSpan {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
z affineSpan R {x, y}
theorem wbtw_iff_right_eq_or_left_mem_image_Ici {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} :
Wbtw R x y z z = y x () ''
theorem Wbtw.left_mem_image_Ici_of_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hne : z y) :
x () ''
theorem Wbtw.left_mem_affineSpan_of_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hne : z y) :
x affineSpan R {z, y}
theorem sbtw_iff_right_ne_and_left_mem_image_Ioi {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} :
Sbtw R x y z z y x () ''
theorem Sbtw.left_mem_image_Ioi {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
x () ''
theorem Sbtw.left_mem_affineSpan {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Sbtw R x y z) :
x affineSpan R {z, y}
theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_le {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (v : V) {r₁ : R} {r₂ : R} (hr₁ : 0 r₁) (hr₂ : r₁ r₂) :
Wbtw R x (r₁ v +ᵥ x) (r₂ v +ᵥ x)
theorem wbtw_or_wbtw_smul_vadd_of_nonneg {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (v : V) {r₁ : R} {r₂ : R} (hr₁ : 0 r₁) (hr₂ : 0 r₂) :
Wbtw R x (r₁ v +ᵥ x) (r₂ v +ᵥ x) Wbtw R x (r₂ v +ᵥ x) (r₁ v +ᵥ x)
theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_le {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (v : V) {r₁ : R} {r₂ : R} (hr₁ : r₁ 0) (hr₂ : r₂ r₁) :
Wbtw R x (r₁ v +ᵥ x) (r₂ v +ᵥ x)
theorem wbtw_or_wbtw_smul_vadd_of_nonpos {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (v : V) {r₁ : R} {r₂ : R} (hr₁ : r₁ 0) (hr₂ : r₂ 0) :
Wbtw R x (r₁ v +ᵥ x) (r₂ v +ᵥ x) Wbtw R x (r₂ v +ᵥ x) (r₁ v +ᵥ x)
theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (v : V) {r₁ : R} {r₂ : R} (hr₁ : r₁ 0) (hr₂ : 0 r₂) :
Wbtw R (r₁ v +ᵥ x) x (r₂ v +ᵥ x)
theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (v : V) {r₁ : R} {r₂ : R} (hr₁ : 0 r₁) (hr₂ : r₂ 0) :
Wbtw R (r₁ v +ᵥ x) x (r₂ v +ᵥ x)
theorem Wbtw.trans_left_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) :
Wbtw R x y z
theorem Wbtw.trans_right_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Wbtw R w x z) (h₂ : Wbtw R x y z) :
Wbtw R w x y
theorem Sbtw.trans_left_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Sbtw R w y z) (h₂ : Sbtw R w x y) :
Sbtw R x y z
theorem Sbtw.trans_right_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {w : P} {x : P} {y : P} {z : P} (h₁ : Sbtw R w x z) (h₂ : Sbtw R x y z) :
Sbtw R w x y
theorem Wbtw.collinear {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Wbtw R x y z) :
Collinear R {x, y, z}
theorem Collinear.wbtw_or_wbtw_or_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} (h : Collinear R {x, y, z}) :
Wbtw R x y z Wbtw R y z x Wbtw R z x y
theorem wbtw_iff_sameRay_vsub {R : Type u_1} {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} {z : P} :
Wbtw R x y z SameRay R (y -ᵥ x) (z -ᵥ y)
theorem wbtw_pointReflection (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (y : P) :
Wbtw R y x ( y)
theorem sbtw_pointReflection_of_ne (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} (h : x y) :
Sbtw R y x ( y)
theorem wbtw_midpoint (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [Module R V] [] (x : P) (y : P) :
Wbtw R x (midpoint R x y) y
theorem sbtw_midpoint_of_ne (R : Type u_1) {V : Type u_2} {P : Type u_4} [] [Module R V] [] {x : P} {y : P} (h : x y) :
Sbtw R x (midpoint R x y) y