perpBisector_ne_bot

Mathlib.Geometry.Euclidean.PerpBisector

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

English

The perpBisector is not the bottom subspace.

Русский

ПерпBisector не равно нижнему подпространству.

LaTeX

$$$\perpBisector(p_1,p_2) \neq \bot$$$

Lean4

@[simp]
theorem perpBisector_ne_bot : perpBisector p₁ p₂ ≠ ⊥ := by rw [← nonempty_iff_ne_bot]; exact perpBisector_nonempty

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

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

Разделы

Аффилиация

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