Collinear.sbtw_of_dist_eq_of_dist_lt
theorem Collinear.sbtw_of_dist_eq_of_dist_lt :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
[inst_2 : StrictConvexSpace ℝ V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {p p₁ p₂ p₃ : P}
{r : ℝ}, Collinear ℝ {p₁, p₂, p₃} → dist p₁ p = r → dist p₂ p < r → dist p₃ p = r → p₁ ≠ p₃ → Sbtw ℝ p₁ p₂ p₃
The theorem `Collinear.sbtw_of_dist_eq_of_dist_lt` states that given three points (`p₁`, `p₂`, `p₃`) which lie on the same straight line (are collinear), where `p₁` and `p₃` are distinct points and both are at a distance `r` from a point `p`, and `p₂` is at a distance less than `r` from `p`, then `p₂` is strictly between `p₁` and `p₃`. Here, being strictly between means that `p₂` is within the segment `p₁p₃` but is not equal to either `p₁` or `p₃`.
More concisely: Given three collinear points `p₁`, `p₂`, `p₃` with `p₁ ≠ p₃`, `dist (p₁, p) = dist (p₃, p) = r`, and `dist (p₂, p) < r`, then `p₂` lies strictly between `p₁` and `p₃`.
|
Collinear.wbtw_of_dist_eq_of_dist_le
theorem Collinear.wbtw_of_dist_eq_of_dist_le :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
[inst_2 : StrictConvexSpace ℝ V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {p p₁ p₂ p₃ : P}
{r : ℝ}, Collinear ℝ {p₁, p₂, p₃} → dist p₁ p = r → dist p₂ p ≤ r → dist p₃ p = r → p₁ ≠ p₃ → Wbtw ℝ p₁ p₂ p₃
The theorem `Collinear.wbtw_of_dist_eq_of_dist_le` states that given three collinear points (`p₁`, `p₂`, `p₃`) in a pseudo-metric space associated with a normed and strictly convex space over the real numbers, where `p₁` and `p₃` are at distance `r` from a point `p` and `p₂` is at a distance less than or equal to `r` from `p`, if `p₁` and `p₃` are distinct, then `p₂` is weakly between `p₁` and `p₃`. In simpler terms, if three points are on the same line and two of them are the same distance from a reference point `p` while the third one is closer to or at the same distance with `p`, then the third point lies in between the other two.
More concisely: Given three collinear points `p₁`, `p₂`, `p₃` in a normed and strictly convex space over the real numbers, if `∥p₁ - p∥` = `∥p₃ - p∥` and `∥p₂ - p∥ ≤ ∥p₁ - p∥`, then `p₂` is weakly between `p₁` and `p₃`.
|
dist_add_dist_eq_iff
theorem dist_add_dist_eq_iff :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
[inst_2 : StrictConvexSpace ℝ V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {a b c : P},
dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
In a strictly convex space, the theorem states that the sum of the distance from point 'a' to point 'b' and the distance from point 'b' to point 'c' is equal to the distance from point 'a' to point 'c' if and only if point 'b' is weakly between point 'a' and point 'c'. This is a condition that turns the triangle inequality into an equality. The weak betweenness is defined in terms of affine segments, which means that the point 'b' lies on the line segment joining 'a' and 'c'.
More concisely: In a strictly convex space, the triangle equality holds if and only if the midpoint of the segment connecting points 'a' and 'c' lies on the segment connecting points 'a' and 'b'.
|