perpBisector_self

Mathlib.Geometry.Euclidean.PerpBisector

URI: https://scilib.ai/kg/mathlib#AffineSubspace.perpBisector_self

English

The perpBisector of p lies at the top element if and only if p1 = p2 in the affine lattice sense.

Русский

Перпендикулярный бисектор от p равен вершинному элементу тогда, когда p1 = p2 в аффинной решётке.

LaTeX

$$$\perpBisector(p,p) = \top$$$

Lean4

@[simp]
theorem perpBisector_self (p : P) : perpBisector p p = ⊤ :=
  top_unique fun _ ↦ by simp [mem_perpBisector_iff_inner_eq_inner]

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

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

Разделы

Аффилиация

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