mem_perpBisector_iff_dist_eq'

Mathlib.Geometry.Euclidean.PerpBisector

URI: https://scilib.ai/kg/mathlib#AffineSubspace.mem_perpBisector_iff_dist_eq'

English

For any p1, p2, perpBisector(p1,p2) = perpBisector(p2,p1).

Русский

Для любых p1, p2 равенство perpBisector(p1,p2) = perpBisector(p2,p1).

LaTeX

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

Lean4

theorem mem_perpBisector_iff_dist_eq' : c ∈ perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c := by
  simp only [mem_perpBisector_iff_dist_eq, dist_comm]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru