English
If dist x y equals r times dist x z and dist y z equals (1 - r) times dist x z, then y equals lineMap x z r.
Русский
Если dist(x,y) = r dist(x,z) и dist(y,z) = (1-r) dist(x,z), то y равно линейной карте lineMap x z r.
LaTeX
$$$dist(x,y) = r\, dist(x,z) \quad \wedge\quad dist(y,z) = (1-r)\, dist(x,z) \Rightarrow y = \mathrm{lineMap}(x,z,r)$$$
Lean4
/-- In a strictly convex space, the triangle inequality turns into an equality if and only if the
middle point belongs to the segment joining two other points. -/
theorem dist_add_dist_eq_iff : dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c :=
by
have :
dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ segment ℝ (a -ᵥ a) (c -ᵥ a) :=
by simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel', eq_comm]
simp_rw [dist_vsub_cancel_right, ← affineSegment_eq_segment, ← affineSegment_vsub_const_image] at this
rwa [(vsub_left_injective _).mem_set_image] at this
