mathlib documentation

analysis.convex.strict_convex_between

Betweenness in affine spaces for strictly convex spaces #

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} [normed_add_comm_group V] [normed_space V] [pseudo_metric_space P] [normed_add_torsor V P] [strict_convex_space V] (p : P) {p₁ p₂ p₃ : P} (h : sbtw p₁ p₂ p₃) :
theorem wbtw.dist_le_max_dist {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space V] [pseudo_metric_space P] [normed_add_torsor V P] [strict_convex_space V] (p : P) {p₁ p₂ p₃ : P} (h : wbtw p₁ p₂ p₃) :
theorem collinear.wbtw_of_dist_eq_of_dist_le {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space V] [pseudo_metric_space P] [normed_add_torsor V P] [strict_convex_space V] {p p₁ p₂ p₃ : P} {r : } (h : collinear {p₁, p₂, p₃}) (hp₁ : has_dist.dist p₁ p = r) (hp₂ : has_dist.dist p₂ p r) (hp₃ : has_dist.dist p₃ p = r) (hp₁p₃ : p₁ p₃) :
wbtw 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} [normed_add_comm_group V] [normed_space V] [pseudo_metric_space P] [normed_add_torsor V P] [strict_convex_space V] {p p₁ p₂ p₃ : P} {r : } (h : collinear {p₁, p₂, p₃}) (hp₁ : has_dist.dist p₁ p = r) (hp₂ : has_dist.dist p₂ p < r) (hp₃ : has_dist.dist p₃ p = r) (hp₁p₃ : p₁ p₃) :
sbtw 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.