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