orthocenter_eq_mongePoint

Mathlib.Geometry.Euclidean.MongePoint

URI: https://scilib.ai/kg/mathlib#Affine.Triangle.orthocenter_eq_mongePoint

English

The orthocenter of a triangle equals its Monge point.

Русский

Ортогцентр треугольника равен его точке Монжа.

LaTeX

$$$t.\text{orthocenter} = t.\text{mongePoint}$$$

Lean4

/-- The orthocenter equals the Monge point. -/
theorem orthocenter_eq_mongePoint (t : Triangle ℝ P) : t.orthocenter = t.mongePoint :=
  rfl

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

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

Разделы

Аффилиация

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