English
The distance from the midpoint to p1 equals the same as from p1 to midpoint, i.e., dist(midpoint, p1) = (2)^{-1} · dist(p1, p2).
Русский
Расстояние от середины до p1 равно расстоянию от p1 до середины: dist(midpoint, p1) = 2^{-1} dist(p1,p2).
LaTeX
$$$\mathrm{dist}(\mathrm{midpoint}\; p_1\; p_2, p_1) = ‖2‖^{-1} \cdot \mathrm{dist}(p_1,p_2)$$$
Lean4
@[simp]
theorem dist_midpoint_left (p₁ p₂ : P) : dist (midpoint 𝕜 p₁ p₂) p₁ = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂ := by
rw [dist_comm, dist_left_midpoint]