dist_circumcenter_reflection_orthocenter

English

The distance from the circumcenter to the reflection of the orthocenter in a side equals the circumradius.

Русский

Расстояние от центра описанной окружности до отражения ортоцентра в сторону равно радиусу описанной окружности.

LaTeX

$$$\operatorname{dist}(O, \text{reflection}_{\text{side}}(H)) = R.$$$

Lean4

/-- The distance from the circumcenter to the reflection of the orthocenter in a side equals the
circumradius. -/
theorem dist_circumcenter_reflection_orthocenter (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h : i₁ ≠ i₂) :
    dist t.circumcenter (reflection (affineSpan ℝ (t.points '' { i₁, i₂ })) t.orthocenter) = t.circumradius := by
  rw [EuclideanGeometry.dist_reflection, dist_comm, dist_orthocenter_reflection_circumcenter t h]

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