dist_orthocenter_reflection_circumcenter_finset

English

A variant of the distance formula using a Finset to describe the side reflection relation.

Русский

Вариант формулы расстояния с использованием конечного множества для описания отражения стороны.

LaTeX

$$$\text{dist}_{\text{finset}}(H, \text{reflection}_{\text{finite set}}(O)) = R$$$

Lean4

/-- The distance from the orthocenter to the reflection of the
circumcenter in a side equals the circumradius, variant using a
`Finset`. -/
theorem dist_orthocenter_reflection_circumcenter_finset (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h : i₁ ≠ i₂) :
    dist t.orthocenter (reflection (affineSpan ℝ (t.points '' ↑({ i₁, i₂ } : Finset (Fin 3)))) t.circumcenter) =
      t.circumradius :=
  by
  simp only [coe_insert, coe_singleton]
  exact dist_orthocenter_reflection_circumcenter _ h

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