# mathlib3documentation

analysis.convex.strict_convex_between

# Betweenness in affine spaces for strictly convex spaces #

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

This file proves results about betweenness for points in an affine space for a strictly convex space.

theorem sbtw.dist_lt_max_dist {V : Type u_1} {P : Type u_2} [ V] [ P] (p : P) {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p < p)
theorem wbtw.dist_le_max_dist {V : Type u_1} {P : Type u_2} [ V] [ P] (p : P) {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p p)
theorem collinear.wbtw_of_dist_eq_of_dist_le {V : Type u_1} {P : Type u_2} [ V] [ P] {p p₁ p₂ p₃ : P} {r : } (h : {p₁, p₂, p₃}) (hp₁ : p = r) (hp₂ : p r) (hp₃ : p = r) (hp₁p₃ : p₁ p₃) :
p₁ p₂ p₃

Given three collinear points, two (not equal) with distance r from p and one with distance at most r from p, the third point is weakly between the other two points.

theorem collinear.sbtw_of_dist_eq_of_dist_lt {V : Type u_1} {P : Type u_2} [ V] [ P] {p p₁ p₂ p₃ : P} {r : } (h : {p₁, p₂, p₃}) (hp₁ : p = r) (hp₂ : p < r) (hp₃ : p = r) (hp₁p₃ : p₁ p₃) :
p₁ p₂ p₃

Given three collinear points, two (not equal) with distance r from p and one with distance less than r from p, the third point is strictly between the other two points.