perpBisector_comm — Mathlib

English

The map c ↦ c is symmetric with respect to the perpendicular bisector; in particular, bisector is unaffected by swapping p1 and p2.

Русский

Перпендикулярный бисектор симметричен относительно обмена p1 и p2; бисектор не меняется при перестановке.

LaTeX

$$$\perpBisector(p_1,p_2) = \perpBisector(p_2,p_1)$$$

Lean4

theorem perpBisector_comm (p₁ p₂ : P) : perpBisector p₁ p₂ = perpBisector p₂ p₁ := by ext c;
  simp only [mem_perpBisector_iff_dist_eq, eq_comm]

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