perpBisector_nonempty

Mathlib.Geometry.Euclidean.PerpBisector

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

English

For any p1,p2 in P there exists a point on the perpendicular bisector of [p1,p2].

Русский

Для любых p1,p2 в P существует точка на перпендикулярном бисекторе отрезка [p1,p2].

LaTeX

$$$\exists c \; c \in \perpBisector(p_1,p_2)$$$

Lean4

theorem perpBisector_nonempty : (perpBisector p₁ p₂ : Set P).Nonempty :=
  ⟨_, midpoint_mem_perpBisector _ _⟩

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

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

Разделы

Аффилиация

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