dist_circumcenter_reflection_orthocenter_finset

English

A Finset variant of the circumcenter-reflection distance identity.

Русский

Финитный вариант тождества расстояния между центром окружности и отражением ортоцентра.

LaTeX

$$$\operatorname{dist}_{\text{finset}}(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, variant using a `Finset`. -/
theorem dist_circumcenter_reflection_orthocenter_finset (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h : i₁ ≠ i₂) :
    dist t.circumcenter (reflection (affineSpan ℝ (t.points '' ↑({ i₁, i₂ } : Finset (Fin 3)))) t.orthocenter) =
      t.circumradius :=
  by
  simp only [coe_insert, coe_singleton]
  exact dist_circumcenter_reflection_orthocenter _ h

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