direction_perpBisector — Mathlib

English

The direction (tangent subspace) of the perpendicular bisector of p1 and p2 is the orthogonal complement of the span of p2 − p1.

Русский

Направление перпендикулярного бисектора p1 и p2 равно орто-комплементу линейного пространства, порождаемого вектором p2 − p1.

LaTeX

$$$\mathrm{direction}(\perpBisector(p_1,p_2)) = (\mathbb{R}\,\cdot (p_2 - p_1))^{\perp}$$$

Lean4

@[simp]
theorem direction_perpBisector (p₁ p₂ : P) : (perpBisector p₁ p₂).direction = (ℝ ∙ (p₂ -ᵥ p₁))ᗮ :=
  by
  rw [perpBisector, direction_mk']
  ext x
  exact Submodule.mem_orthogonal_singleton_iff_inner_right.symm

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