mapsTo_perpBisector

Mathlib.Geometry.Euclidean.PerpBisector

URI: https://scilib.ai/kg/mathlib#Isometry.mapsTo_perpBisector

← MathLib Explorer

English

Isometry maps perpBisector(p1,p2) into perpBisector(f(p1),f(p2)).

Русский

Изометрия отображает perpBisector(p1,p2) в perpBisector(f(p1),f(p2)).

LaTeX

$$MapsTo f (perpBisector(p1,p2)) (perpBisector(f(p1),f(p2)))$$

Lean4

theorem mapsTo_perpBisector {f : P → P'} (h : Isometry f) (p₁ p₂ : P) :
    MapsTo f (perpBisector p₁ p₂) (perpBisector (f p₁) (f p₂)) :=
  (h.preimage_perpBisector p₁ p₂).ge

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

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

Разделы

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

Аффилиация

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