orthocenter_eq_smul_vsub_vadd_circumcenter

English

The orthocenter lies on the Euler line with the circumcenter and centroid, and satisfies H = O + 3(G − O) = 3G − 2O, where O is the circumcenter and G the centroid.

Русский

Ортохоцентр лежит на Эйлеровой прямой вместе сcircumcenter и центроид; выполняется H = O + 3(G − O) = 3G − 2O, где O — центр описанной окружности, G — центр масс вершин.

LaTeX

$$$\text{For a triangle } t,\ H = t.circumcenter + 3\bigl(t.centroid(t.points) - t.circumcenter\bigr).$$$

Lean4

/-- The position of the orthocenter in relation to the circumcenter
and centroid. -/
theorem orthocenter_eq_smul_vsub_vadd_circumcenter (t : Triangle ℝ P) :
    t.orthocenter = (3 : ℝ) • ((univ : Finset (Fin 3)).centroid ℝ t.points -ᵥ t.circumcenter : V) +ᵥ t.circumcenter :=
  by
  rw [orthocenter_eq_mongePoint, mongePoint_eq_smul_vsub_vadd_circumcenter]
  simp

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