mathlib3 documentation

analysis.convex.between

Betweenness in affine spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

source
def affine_segment (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor 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
source
theorem affine_segment_eq_segment (R : Type u_1) {V : Type u_2} [ordered_ring R] [add_comm_group V] [module R V] (x y : V) :
affine_segment R x y = segment R x y
source
theorem affine_segment_comm (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
affine_segment R x y = affine_segment R y x
source
theorem left_mem_affine_segment (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
x ∈ affine_segment R x y
source
theorem right_mem_affine_segment (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
y ∈ affine_segment R x y
source
@[simp]
theorem affine_segment_same (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x : P) :
affine_segment R x x = {x}
source
@[simp]
theorem affine_segment_image {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] (f : P →ᵃ[R] P') (x y : P) :
⇑f '' affine_segment R x y = affine_segment R (⇑f x) (⇑f y)
source
@[simp]
theorem affine_segment_const_vadd_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) (v : V) :
has_vadd.vadd v '' affine_segment R x y = affine_segment R (v +ᵥ x) (v +ᵥ y)
source
@[simp]
theorem affine_segment_vadd_const_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : V) (p : P) :
(λ (_x : V), _x +ᵥ p) '' affine_segment R x y = affine_segment R (x +ᵥ p) (y +ᵥ p)
source
@[simp]
theorem affine_segment_const_vsub_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y p : P) :
has_vsub.vsub p '' affine_segment R x y = affine_segment R (p -ᵥ x) (p -ᵥ y)
source
@[simp]
theorem affine_segment_vsub_const_image (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y p : P) :
(λ (_x : P), _x -ᵥ p) '' affine_segment R x y = affine_segment R (x -ᵥ p) (y -ᵥ p)
source
@[simp]
theorem mem_const_vadd_affine_segment {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (v : V) :
v +ᵥ z ∈ affine_segment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affine_segment R x y
source
@[simp]
theorem mem_vadd_const_affine_segment {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : V} (p : P) :
z +ᵥ p ∈ affine_segment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affine_segment R x y
source
@[simp]
theorem mem_const_vsub_affine_segment {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (p : P) :
p -ᵥ z ∈ affine_segment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affine_segment R x y
source
@[simp]
theorem mem_vsub_const_affine_segment {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (p : P) :
z -ᵥ p ∈ affine_segment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affine_segment R x y
source
def wbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y z : P) :
Prop

The point y is weakly between x and z.

Equations
source
def sbtw (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y z : P) :
Prop

The point y is strictly between x and z.

Equations
source
theorem wbtw.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {x y z : P} (h : wbtw R x y z) (f : P →ᵃ[R] P') :
wbtw R (⇑f x) (⇑f y) (⇑f z)
source
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} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {x y z : P} {f : P →ᵃ[R] P'} (hf : function.injective ⇑f) :
wbtw R (⇑f x) (⇑f y) (⇑f z) ↔ wbtw R x y z
source
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} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {x y z : P} {f : P →ᵃ[R] P'} (hf : function.injective ⇑f) :
sbtw R (⇑f x) (⇑f y) (⇑f z) ↔ sbtw R x y z
source
@[simp]
theorem affine_equiv.wbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {x y z : P} (f : P ≃ᵃ[R] P') :
wbtw R (⇑f x) (⇑f y) (⇑f z) ↔ wbtw R x y z
source
@[simp]
theorem affine_equiv.sbtw_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {x y z : P} (f : P ≃ᵃ[R] P') :
sbtw R (⇑f x) (⇑f y) (⇑f z) ↔ sbtw R x y z
source
@[simp]
theorem wbtw_const_vadd_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (v : V) :
wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ wbtw R x y z
source
@[simp]
theorem wbtw_vadd_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : V} (p : P) :
wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ wbtw R x y z
source
@[simp]
theorem wbtw_const_vsub_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (p : P) :
wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ wbtw R x y z
source
@[simp]
theorem wbtw_vsub_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (p : P) :
wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ wbtw R x y z
source
@[simp]
theorem sbtw_const_vadd_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (v : V) :
sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ sbtw R x y z
source
@[simp]
theorem sbtw_vadd_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : V} (p : P) :
sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ sbtw R x y z
source
@[simp]
theorem sbtw_const_vsub_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (p : P) :
sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ sbtw R x y z
source
@[simp]
theorem sbtw_vsub_const_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (p : P) :
sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ sbtw R x y z
source
theorem sbtw.wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
wbtw R x y z
source
theorem sbtw.ne_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
y ≠ x
source
theorem sbtw.left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
x ≠ y
source
theorem sbtw.ne_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
y ≠ z
source
theorem sbtw.right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
z ≠ y
source
theorem sbtw.mem_image_Ioo {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
y ∈ ⇑(affine_map.line_map x z) '' set.Ioo 0 1
source
theorem wbtw.mem_affine_span {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) :
y ∈ affine_span R {x, z}
source
theorem wbtw_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
wbtw R x y z ↔ wbtw R z y x
source
theorem wbtw.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
wbtw R x y z → wbtw R z y x

Alias of the forward direction of wbtw_comm.

source
theorem sbtw_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
sbtw R x y z ↔ sbtw R z y x
source
theorem sbtw.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
sbtw R x y z → sbtw R z y x

Alias of the forward direction of sbtw_comm.

source
@[simp]
theorem wbtw_self_left (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
wbtw R x x y
source
@[simp]
theorem wbtw_self_right (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
wbtw R x y y
source
@[simp]
theorem wbtw_self_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y : P} :
wbtw R x y x ↔ y = x
source
@[simp]
theorem not_sbtw_self_left (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
¬sbtw R x x y
source
@[simp]
theorem not_sbtw_self_right (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
¬sbtw R x y y
source
theorem wbtw.left_ne_right_of_ne_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) (hne : y ≠ x) :
x ≠ z
source
theorem wbtw.left_ne_right_of_ne_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) (hne : y ≠ z) :
x ≠ z
source
theorem sbtw.left_ne_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
x ≠ z
source
theorem sbtw_iff_mem_image_Ioo_and_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y z : P} :
sbtw R x y z ↔ y ∈ ⇑(affine_map.line_map x z) '' set.Ioo 0 1 ∧ x ≠ z
source
@[simp]
theorem not_sbtw_self (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
¬sbtw R x y x
source
theorem wbtw_swap_left_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y : P} (z : P) :
wbtw R x y z ∧ wbtw R y x z ↔ x = y
source
theorem wbtw_swap_right_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] (x : P) {y z : P} :
wbtw R x y z ∧ wbtw R x z y ↔ y = z
source
theorem wbtw_rotate_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] (x : P) {y z : P} :
wbtw R x y z ∧ wbtw R z x y ↔ x = y
source
theorem wbtw.swap_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y z : P} (h : wbtw R x y z) :
wbtw R y x z ↔ x = y
source
theorem wbtw.swap_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y z : P} (h : wbtw R x y z) :
wbtw R x z y ↔ y = z
source
theorem wbtw.rotate_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y z : P} (h : wbtw R x y z) :
wbtw R z x y ↔ x = y
source
theorem sbtw.not_swap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y z : P} (h : sbtw R x y z) :
¬wbtw R y x z
source
theorem sbtw.not_swap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y z : P} (h : sbtw R x y z) :
¬wbtw R x z y
source
theorem sbtw.not_rotate {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y z : P} (h : sbtw R x y z) :
¬wbtw R z x y
source
@[simp]
theorem wbtw_line_map_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y : P} {r : R} :
wbtw R x (⇑(affine_map.line_map x y) r) y ↔ x = y ∨ r ∈ set.Icc 0 1
source
@[simp]
theorem sbtw_line_map_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {x y : P} {r : R} :
sbtw R x (⇑(affine_map.line_map x y) r) y ↔ x ≠ y ∧ r ∈ set.Ioo 0 1
source
@[simp]
theorem wbtw_mul_sub_add_iff {R : Type u_1} [ordered_ring R] [no_zero_divisors R] {x y r : R} :
wbtw R x (r * (y - x) + x) y ↔ x = y ∨ r ∈ set.Icc 0 1
source
@[simp]
theorem sbtw_mul_sub_add_iff {R : Type u_1} [ordered_ring R] [no_zero_divisors R] {x y r : R} :
sbtw R x (r * (y - x) + x) y ↔ x ≠ y ∧ r ∈ set.Ioo 0 1
source
@[simp]
theorem wbtw_zero_one_iff {R : Type u_1} [ordered_ring R] {x : R} :
wbtw R 0 x 1 ↔ x ∈ set.Icc 0 1
source
@[simp]
theorem wbtw_one_zero_iff {R : Type u_1} [ordered_ring R] {x : R} :
wbtw R 1 x 0 ↔ x ∈ set.Icc 0 1
source
@[simp]
theorem sbtw_zero_one_iff {R : Type u_1} [ordered_ring R] {x : R} :
sbtw R 0 x 1 ↔ x ∈ set.Ioo 0 1
source
@[simp]
theorem sbtw_one_zero_iff {R : Type u_1} [ordered_ring R] {x : R} :
sbtw R 1 x 0 ↔ x ∈ set.Ioo 0 1
source
theorem wbtw.trans_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {w x y z : P} (h₁ : wbtw R w y z) (h₂ : wbtw R w x y) :
wbtw R w x z
source
theorem wbtw.trans_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] {w x y z : P} (h₁ : wbtw R w x z) (h₂ : wbtw R x y z) :
wbtw R w y z
source
theorem wbtw.trans_sbtw_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : wbtw R w y z) (h₂ : sbtw R w x y) :
sbtw R w x z
source
theorem wbtw.trans_sbtw_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : wbtw R w x z) (h₂ : sbtw R x y z) :
sbtw R w y z
source
theorem sbtw.trans_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : sbtw R w y z) (h₂ : sbtw R w x y) :
sbtw R w x z
source
theorem sbtw.trans_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : sbtw R w x z) (h₂ : sbtw R x y z) :
sbtw R w y z
source
theorem wbtw.trans_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : wbtw R w y z) (h₂ : wbtw R w x y) (h : y ≠ z) :
x ≠ z
source
theorem wbtw.trans_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : wbtw R w x z) (h₂ : wbtw R x y z) (h : w ≠ x) :
w ≠ y
source
theorem sbtw.trans_wbtw_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : sbtw R w y z) (h₂ : wbtw R w x y) :
x ≠ z
source
theorem sbtw.trans_wbtw_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors R V] {w x y z : P} (h₁ : sbtw R w x z) (h₂ : wbtw R x y z) :
w ≠ y
source
theorem sbtw.affine_combination_of_mem_affine_span_pair {R : Type u_1} {V : Type u_2} {P : Type u_4} [ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_divisors R] [no_zero_smul_divisors R V] {ι : Type u_3} {p : ι → P} (ha : affine_independent R p) {w w₁ w₂ : ι → R} {s : finset ι} (hw : s.sum (λ (i : ι), w i) = 1) (hw₁ : s.sum (λ (i : ι), w₁ i) = 1) (hw₂ : s.sum (λ (i : ι), w₂ i) = 1) (h : ⇑(finset.affine_combination R s p) w ∈ affine_span R {⇑(finset.affine_combination R s p) w₁, ⇑(finset.affine_combination R s p) w₂}) {i : ι} (his : i ∈ s) (hs : sbtw R (w₁ i) (w i) (w₂ i)) :
sbtw R (⇑(finset.affine_combination R s p) w₁) (⇑(finset.affine_combination R s p) w) (⇑(finset.affine_combination R s p) w₂)
source
theorem wbtw.same_ray_vsub {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) :
same_ray R (y -ᵥ x) (z -ᵥ y)
source
theorem wbtw.same_ray_vsub_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) :
same_ray R (y -ᵥ x) (z -ᵥ x)
source
theorem wbtw.same_ray_vsub_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) :
same_ray R (z -ᵥ x) (z -ᵥ y)
source
theorem sbtw_of_sbtw_of_sbtw_of_mem_affine_span_pair {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_ring R] [add_comm_group V] [module R V] [add_torsor V P] [no_zero_smul_divisors 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 ∈ affine_span R {t.points i₁, p₁}) (h₂' : p ∈ affine_span 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.

source
theorem wbtw_iff_left_eq_or_right_mem_image_Ici {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
wbtw R x y z ↔ x = y ∨ z ∈ ⇑(affine_map.line_map x y) '' set.Ici 1
source
theorem wbtw.right_mem_image_Ici_of_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) (hne : x ≠ y) :
z ∈ ⇑(affine_map.line_map x y) '' set.Ici 1
source
theorem wbtw.right_mem_affine_span_of_left_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) (hne : x ≠ y) :
z ∈ affine_span R {x, y}
source
theorem sbtw_iff_left_ne_and_right_mem_image_IoI {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(affine_map.line_map x y) '' set.Ioi 1
source
theorem sbtw.right_mem_image_Ioi {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
z ∈ ⇑(affine_map.line_map x y) '' set.Ioi 1
source
theorem sbtw.right_mem_affine_span {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
z ∈ affine_span R {x, y}
source
theorem wbtw_iff_right_eq_or_left_mem_image_Ici {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
wbtw R x y z ↔ z = y ∨ x ∈ ⇑(affine_map.line_map z y) '' set.Ici 1
source
theorem wbtw.left_mem_image_Ici_of_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) (hne : z ≠ y) :
x ∈ ⇑(affine_map.line_map z y) '' set.Ici 1
source
theorem wbtw.left_mem_affine_span_of_right_ne {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) (hne : z ≠ y) :
x ∈ affine_span R {z, y}
source
theorem sbtw_iff_right_ne_and_left_mem_image_IoI {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
sbtw R x y z ↔ z ≠ y ∧ x ∈ ⇑(affine_map.line_map z y) '' set.Ioi 1
source
theorem sbtw.left_mem_image_Ioi {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
x ∈ ⇑(affine_map.line_map z y) '' set.Ioi 1
source
theorem sbtw.left_mem_affine_span {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : sbtw R x y z) :
x ∈ affine_span R {z, y}
source
theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_le {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁) (hr₂ : r₁ ≤ r₂) :
wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
source
theorem wbtw_or_wbtw_smul_vadd_of_nonneg {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor 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)
source
theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_le {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] (x : P) (v : V) {r₁ r₂ : R} (hr₁ : r₁ ≤ 0) (hr₂ : r₂ ≤ r₁) :
wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
source
theorem wbtw_or_wbtw_smul_vadd_of_nonpos {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor 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)
source
theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] (x : P) (v : V) {r₁ r₂ : R} (hr₁ : r₁ ≤ 0) (hr₂ : 0 ≤ r₂) :
wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
source
theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁) (hr₂ : r₂ ≤ 0) :
wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
source
theorem wbtw.trans_left_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {w x y z : P} (h₁ : wbtw R w y z) (h₂ : wbtw R w x y) :
wbtw R x y z
source
theorem wbtw.trans_right_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {w x y z : P} (h₁ : wbtw R w x z) (h₂ : wbtw R x y z) :
wbtw R w x y
source
theorem sbtw.trans_left_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {w x y z : P} (h₁ : sbtw R w y z) (h₂ : sbtw R w x y) :
sbtw R x y z
source
theorem sbtw.trans_right_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {w x y z : P} (h₁ : sbtw R w x z) (h₂ : sbtw R x y z) :
sbtw R w x y
source
theorem wbtw.collinear {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} (h : wbtw R x y z) :
collinear R {x, y, z}
source
theorem collinear.wbtw_or_wbtw_or_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor 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
source
theorem wbtw_iff_same_ray_vsub {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y z : P} :
wbtw R x y z ↔ same_ray R (y -ᵥ x) (z -ᵥ y)
source
theorem wbtw_point_reflection (R : Type u_1) {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
wbtw R y x (⇑(affine_equiv.point_reflection R x) y)
source
theorem sbtw_point_reflection_of_ne (R : Type u_1) {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y : P} (h : x ≠ y) :
sbtw R y x (⇑(affine_equiv.point_reflection R x) y)
source
theorem wbtw_midpoint (R : Type u_1) {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
wbtw R x (midpoint R x y) y
source
theorem sbtw_midpoint_of_ne (R : Type u_1) {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {x y : P} (h : x ≠ y) :
sbtw R x (midpoint R x y) y