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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x 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

• affineSegment R x y = ⇑(AffineMap.lineMap x y) '' Set.Icc 0 1

theorem affineSegment_eq_segment (R : Type u_1) {V : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] (x y : V) : affineSegment R x y = segment R x y

theorem affineSegment_comm (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : affineSegment R x y = affineSegment R y x

theorem left_mem_affineSegment (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : x ∈ affineSegment R x y

theorem right_mem_affineSegment (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : y ∈ affineSegment R x y

@[simp]

theorem affineSegment_same (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) : affineSegment R x x = {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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] (f : P →ᵃ[R] P') (x y : P) : ⇑f '' affineSegment R x y = affineSegment R (f x) (f y)

@[simp]

theorem affineSegment_const_vadd_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) (v : V) : (fun (x : P) => v +ᵥ x) '' affineSegment R x y = affineSegment R (v +ᵥ x) (v +ᵥ y)

@[simp]

theorem affineSegment_vadd_const_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : V) (p : P) : (fun (x : V) => x +ᵥ p) '' affineSegment R x y = affineSegment R (x +ᵥ p) (y +ᵥ p)

@[simp]

theorem affineSegment_const_vsub_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y p : P) : (fun (x : P) => p -ᵥ x) '' affineSegment R x y = affineSegment R (p -ᵥ x) (p -ᵥ y)

@[simp]

theorem affineSegment_vsub_const_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y p : P) : (fun (x : P) => x -ᵥ p) '' affineSegment R x y = affineSegment R (x -ᵥ p) (y -ᵥ p)

@[simp]

theorem mem_const_vadd_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} (v : V) : v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y

@[simp]

theorem mem_vadd_const_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : V} (p : P) : z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y

@[simp]

theorem mem_const_vsub_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} (p : P) : p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y

@[simp]

theorem mem_vsub_const_affineSegment {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} (p : P) : z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y

def Wbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y z : P) : Prop

The point y is weakly between x and z.

Equations

• Wbtw R x y z = (y ∈ affineSegment R x z)

def Sbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y z : P) : Prop

The point y is strictly between x and z.

Equations

• Sbtw R x y z = (Wbtw R x y z ∧ y ≠ x ∧ y ≠ z)

theorem mem_segment_iff_wbtw {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] {x y z : V} : y ∈ segment R x z ↔ Wbtw R x y z

theorem Wbtw.mem_segment {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] {x y z : V} : Wbtw R x y z → y ∈ segment R x z

Alias of the reverse direction of mem_segment_iff_wbtw.

theorem Convex.mem_of_wbtw {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] {p₀ p₁ p₂ : V} {s : Set V} (hs : Convex R s) (h₀₁₂ : Wbtw R p₀ p₁ p₂) (h₀ : p₀ ∈ s) (h₂ : p₂ ∈ s) : p₁ ∈ s

theorem AffineSubspace.mem_of_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxyz : Wbtw R x y z) (hx : x ∈ s) (hz : z ∈ s) : y ∈ s

theorem 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] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {x y z : P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {x y z : P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} (h : Sbtw R x y z) : y ∈ ⇑(AffineMap.lineMap x z) '' Set.Ioo 0 1

theorem Wbtw.mem_affineSpan {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} : Wbtw R x y z → Wbtw 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} : Sbtw R x y z → Sbtw 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : Wbtw R x x y

@[simp]

theorem wbtw_self_right (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : Wbtw R x y y

@[simp]

theorem wbtw_self_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y z : P} : Sbtw R x y z ↔ y ∈ ⇑(AffineMap.lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z

@[simp]

theorem not_sbtw_self (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : ¬Sbtw R x y x

theorem wbtw_swap_left_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] (x : P) {y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] (x : P) {y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y : P} {r : R} : Wbtw R x ((AffineMap.lineMap x y) 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {x y : P} {r : R} : Sbtw R x ((AffineMap.lineMap x y) r) y ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1

@[simp]

theorem wbtw_mul_sub_add_iff {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] {x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] {x : R} : Wbtw R 0 x 1 ↔ x ∈ Set.Icc 0 1

@[simp]

theorem wbtw_one_zero_iff {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] {x : R} : Wbtw R 1 x 0 ↔ x ∈ Set.Icc 0 1

@[simp]

theorem sbtw_zero_one_iff {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] {x : R} : Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1

@[simp]

theorem sbtw_one_zero_iff {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] {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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {w x y 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} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroDivisors R] [NoZeroSMulDivisors R V] {ι : Type u_6} {p : ι → P} (ha : AffineIndependent R p) {w w₁ w₂ : ι → R} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (h : (Finset.affineCombination R s p) w ∈ affineSpan R {(Finset.affineCombination R s p) w₁, (Finset.affineCombination R s p) w₂}) {i : ι} (his : i ∈ s) (hs : Sbtw R (w₁ i) (w i) (w₂ i)) : Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w) ((Finset.affineCombination R s p) w₂)

theorem Wbtw.sameRay_vsub {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NoZeroSMulDivisors R V] {t : Affine.Triangle R P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) {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_of_le {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x y z : R} (hxz : x ≤ z) : Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

theorem Wbtw.of_le_of_le {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x y z : R} (hxy : x ≤ y) (hyz : y ≤ z) : Wbtw R x y z

theorem Sbtw.of_lt_of_lt {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x y z : R} (hxy : x < y) (hyz : y < z) : Sbtw R x y z

theorem wbtw_iff_left_eq_or_right_mem_image_Ici {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] {x y z : P} : Wbtw R x y z ↔ x = y ∨ z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ici 1

theorem Wbtw.right_mem_image_Ici_of_left_ne {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] {x y z : P} (h : Wbtw R x y z) (hne : x ≠ y) : z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ici 1

theorem Wbtw.right_mem_affineSpan_of_left_ne {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] {x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} : Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ioi 1

theorem Sbtw.right_mem_image_Ioi {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] {x y z : P} (h : Sbtw R x y z) : z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ioi 1

theorem Sbtw.right_mem_affineSpan {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] {x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} : Wbtw R x y z ↔ z = y ∨ x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ici 1

theorem Wbtw.left_mem_image_Ici_of_right_ne {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] {x y z : P} (h : Wbtw R x y z) (hne : z ≠ y) : x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ici 1

theorem Wbtw.left_mem_affineSpan_of_right_ne {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] {x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} : Sbtw R x y z ↔ z ≠ y ∧ x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ioi 1

theorem Sbtw.left_mem_image_Ioi {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] {x y z : P} (h : Sbtw R x y z) : x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ioi 1

theorem Sbtw.left_mem_affineSpan {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] {x y z : P} (h : Sbtw R x y z) : x ∈ affineSpan R {z, y}

theorem AffineSubspace.right_mem_of_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] {x y z : P} {s : AffineSubspace R P} (hxyz : Wbtw R x y z) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : z ∈ s

theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_le {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] (x : P) (v : V) {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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (v : V) {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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (v : V) {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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (v : V) {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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (v : V) {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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (v : V) {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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {w x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {w x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {w x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {w x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P} : Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y)

theorem AffineIndependent.not_wbtw_of_injective {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] {ι : Type u_6} (i j k : ι) (h : Function.Injective ![i, j, k]) {T : ι → P} (hT : AffineIndependent R T) : ¬Wbtw R (T i) (T j) (T k)

If T is an affine independent family of points, then any 3 distinct points form a triangle.

theorem wbtw_pointReflection (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] (x y : P) : Wbtw R y x ((AffineEquiv.pointReflection R x) y)

theorem sbtw_pointReflection_of_ne (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] {x y : P} (h : x ≠ y) : Sbtw R y x ((AffineEquiv.pointReflection R x) y)

theorem wbtw_midpoint (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] (x 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} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y : P} (h : x ≠ y) : Sbtw R x (midpoint R x y) y