English
In a strictly convex space, dist a c is strictly less than dist a b + dist b c iff b is not weakly between a, c.
Русский
В строго выпуклом пространстве расстояние dist a c строго меньше dist a b + dist b c тогда, когда b не находится между a и c в слабом смысле.
LaTeX
$$$\dist a c < \dist a b + \dist b c \;\Leftrightarrow\; \neg Wbtw ℝ a b c$$$
Lean4
theorem eq_midpoint_of_dist_eq_half (hx : dist x y = dist x z / 2) (hy : dist y z = dist x z / 2) :
y = midpoint ℝ x z := by
apply eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
· rwa [invOf_eq_inv, ← div_eq_inv_mul]
· rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_mul]