English
Let v be an inner product space over R and P a metric affine space modeled on v. For points p1, p2 in P and any c in P, c lies on the perpendicular bisector of the segment [p1, p2] if and only if the vector from the midpoint of p1 and p2 to c is orthogonal to p2 − p1; equivalently, ⟪c − midpoint(p1, p2), p2 − p1⟫ = 0.
Русский
Пусть V — векторное евклидово пространство над R и P — аффинное пространство с заданным скалярным произведением. Для точек p1, p2 ∈ P и любой c ∈ P точка c лежит на перпендикулярном бисектору отрезка [p1, p2] тогда и только тогда, когда вектор c − midpoint(p1, p2) ортогонален p2 − p1; то есть ⟪c − midpoint(p1, p2), p2 − p1⟫ = 0.
LaTeX
$$$c \in \perpBisector(p_1,p_2) \;\iff\; \langle c - \text{midpoint}(p_1,p_2),\; p_2 - p_1 \rangle = 0$$$
Lean4
/-- A point `c` belongs the perpendicular bisector of `[p₁, p₂] iff `c -ᵥ midpoint ℝ p₁ p₂` is
orthogonal to `p₂ -ᵥ p₁`. -/
theorem mem_perpBisector_iff_inner_eq_zero : c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 :=
inner_eq_zero_symm
