orthocenter_mem_affineSpan — Mathlib

English

The orthocenter lies in the affine span of the triangle's vertices.

Русский

Ортогцентр принадлежит аффинному замыканию вершин треугольника.

LaTeX

$$$t.\text{orthocenter} \in \operatorname{affineSpan}(\mathbb{R})\bigl(\{t.\text{points}_i : i \in \mathrm{Fin}~3\}\bigr).$$$

Lean4

/-- The orthocenter lies in the affine span. -/
theorem orthocenter_mem_affineSpan (t : Triangle ℝ P) : t.orthocenter ∈ affineSpan ℝ (Set.range t.points) :=
  t.mongePoint_mem_affineSpan

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