dist_left_midpoint_eq_dist_right_midpoint

English

The distance from either endpoint to the midpoint is the same: dist(p1, midpoint) = dist(p2, midpoint).

Русский

Расстояние от концов до середины равно друг другу: dist(p1, середина) = dist(p2, середина).

LaTeX

$$$\mathrm{dist}(p_1, \mathrm{midpoint}\; p_1\; p_2) = \mathrm{dist}(p_2, \mathrm{midpoint}\; p_1\; p_2)$$$

Lean4

/-- The midpoint of the segment AB is the same distance from A as it is from B. -/
theorem dist_left_midpoint_eq_dist_right_midpoint (p₁ p₂ : P) :
    dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂) := by
  rw [dist_left_midpoint p₁ p₂, dist_right_midpoint p₁ p₂]

Похожие утверждения