English
Two distinct points are equidistant from a third point if and only if that third point is a rotated version of the vector between the two points by π/2 plus the midpoint of the two points.
Русский
Две различные точки эквидистантны третьей точке тогда и только тогда третья точка равна вращению вектора между двумя точками на π/2 плюс середина между ними.
LaTeX
$$$dist(p_1,p) = dist(p_2,p) \iff \exists r\in\mathbb{R}, r \cdot o.rotation(\tfrac{\pi}{2}) (p_2-p_1) + \mathrm{midpoint}(p_1,p_2) = p$$$
Lean4
/-- Two different points are equidistant from a third point if and only if that third point
equals some multiple of a `π / 2` rotation of the vector between those points, plus the midpoint
of those points. -/
theorem dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint {p₁ p₂ p : P} (h : p₁ ≠ p₂) :
dist p₁ p = dist p₂ p ↔ ∃ r : ℝ, r • o.rotation (π / 2 : ℝ) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p :=
by
refine ⟨fun hd => ?_, fun hr => ?_⟩
· have hi : ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0 :=
by
rw [@dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, ← mul_self_inj (norm_nonneg _) (norm_nonneg _), ←
real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm] at hd
simp_rw [vsub_midpoint, ← vsub_sub_vsub_cancel_left p₂ p₁ p, inner_sub_left, inner_add_right, inner_smul_right,
hd, real_inner_comm (p -ᵥ p₁)]
abel
rw [@Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two V _ _ _ o,
or_iff_right (vsub_ne_zero.2 h.symm)] at hi
rcases hi with ⟨r, hr⟩
rw [eq_comm, ← eq_vadd_iff_vsub_eq] at hr
exact ⟨r, hr.symm⟩
· rcases hr with ⟨r, rfl⟩
simp_rw [@dist_eq_norm_vsub V, vsub_vadd_eq_vsub_sub, left_vsub_midpoint, right_vsub_midpoint, invOf_eq_inv, ←
neg_vsub_eq_vsub_rev p₂ p₁, ← mul_self_inj (norm_nonneg _) (norm_nonneg _), ← real_inner_self_eq_norm_mul_norm,
inner_sub_sub_self]
simp [-neg_vsub_eq_vsub_rev]
