orthocenter_vsub_circumcenter_eq_sum_vsub

English

The difference between the orthocenter and circumcenter equals the sum of the vertex displacements from the circumcenter: H − O = ∑i (A_i − O).

Русский

Разность ортоцентра и центра описанной окружности равна сумме векторов от центра окружности к вершинам треугольника: H − O = ∑(A_i − O).

LaTeX

$$$t.\text{orthocenter} -\!\!\text{circumcenter} = \sum_i (t.points_i -\!\!\text{circumcenter}).$$$

Lean4

/-- **Sylvester's theorem**, specialized to triangles. -/
theorem orthocenter_vsub_circumcenter_eq_sum_vsub (t : Triangle ℝ P) :
    t.orthocenter -ᵥ t.circumcenter = ∑ i, (t.points i -ᵥ t.circumcenter) := by
  rw [← t.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, zero_add, one_smul, orthocenter_eq_mongePoint]

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