perpBisector_eq_top

Mathlib.Geometry.Euclidean.PerpBisector

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

← MathLib Explorer

English

The perpBisector equals the top subspace iff p1 = p2.

Русский

ПерпBisector равен верхнему сомножителю тогда и только тогда, когда p1 = p2.

LaTeX

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

Lean4

@[simp]
theorem perpBisector_eq_top : perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ perpBisector_self _⟩
  rw [← left_mem_perpBisector, h]
  trivial

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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