Documentation

Mathlib.Analysis.Convex.StrictConvexBetween

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} [NormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] [StrictConvexSpace V] (p : P) {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw p₁ p₂ p₃) :
dist p₂ p < max (dist p₁ p) (dist p₃ p)
theorem Wbtw.dist_le_max_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] [StrictConvexSpace V] (p : P) {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw p₁ p₂ p₃) :
dist p₂ p max (dist p₁ p) (dist p₃ p)
theorem Collinear.wbtw_of_dist_eq_of_dist_le {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] [StrictConvexSpace V] {p : P} {p₁ : P} {p₂ : P} {p₃ : P} {r : } (h : Collinear {p₁, p₂, p₃}) (hp₁ : dist p₁ p = r) (hp₂ : dist p₂ p r) (hp₃ : 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} [NormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] [StrictConvexSpace V] {p : P} {p₁ : P} {p₂ : P} {p₃ : P} {r : } (h : Collinear {p₁, p₂, p₃}) (hp₁ : dist p₁ p = r) (hp₂ : dist p₂ p < r) (hp₃ : 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.