orthocenter — Mathlib

English

For any triangle, the orthocenter is the Monge point of the triangle.

Русский

Для любого треугольника ортогцентр совпадает с точкой Монжа треугольника.

LaTeX

$$$\text{For a triangle } t,\ \operatorname{orthocenter}(t) = \operatorname{mongePoint}(t).$$$

Lean4

/-- The orthocenter of a triangle is the intersection of its
altitudes.  It is defined here as the 2-dimensional case of the
Monge point. -/
def orthocenter (t : Triangle ℝ P) : P :=
  t.mongePoint

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