mem_perpBisector_iff_inner_eq_zero'

English

A point lies on the perpendicular bisector of p1p2 exactly when the inner product with p2-p1 vanishes after subtracting the midpoint from the point.

Русский

Точка лежит на perpBisector(p1,p2) тогда и только тогда, когда скалярное произведение с вектором p2-p1 равно нулю после вычитания середины из точки.

LaTeX

$$$c \\in \\mathrm{perpBisector}(p_1,p_2) \\iff \\langle p_2-p_1, c - m \\rangle = 0$, где $m = \\mathrm{midpoint}_{\\mathbb{R}}(p_1,p_2).$$$

Lean4

/-- A point `c` belongs the perpendicular bisector of `[p₁, p₂] iff `p₂ -ᵥ p₁` is orthogonal to
`c -ᵥ midpoint ℝ p₁ p₂`. -/
theorem mem_perpBisector_iff_inner_eq_zero' : c ∈ perpBisector p₁ p₂ ↔ ⟪p₂ -ᵥ p₁, c -ᵥ midpoint ℝ p₁ p₂⟫ = 0 :=
  Iff.rfl

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