English
All triangles in an orthocentric system have the same circumradius; there exists a real number r such that every triangle whose vertices lie in s has circumradius r.
Русский
Все треугольники в ортокцентрической системе имеют одинаковый радиус описанной окружности; существует некоторое число r так, что любой треугольник с вершинами в s имеет радиус описанной окружности r.
LaTeX
$$$\\exists r \\in \\mathbb{R}, \\; \\forall t : \\text{Triangle } \\mathbb{R} P,\\; \\mathrm{range}(t.points) \\subseteq s \\; \\to\\; t.circumradius = r$$$
Lean4
/-- All triangles in an orthocentric system have the same circumradius. -/
theorem exists_circumradius_eq {s : Set P} (ho : OrthocentricSystem s) :
∃ r : ℝ, ∀ t : Triangle ℝ P, Set.range t.points ⊆ s → t.circumradius = r :=
by
rcases ho with ⟨t, hto, hts⟩
use t.circumradius
intro t₂ ht₂
have ht₂s := ht₂
rw [hts] at ht₂
rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto ht₂ t₂.independent.injective with ⟨c, hc, h⟩
rw [Set.forall_mem_range] at h
have hs : Set.range t.points ⊆ s := by
rw [hts]
exact Set.subset_insert _ _
rw [affineSpan_of_orthocentricSystem ⟨t, hto, hts⟩ hs t.independent.injective, ←
affineSpan_of_orthocentricSystem ⟨t, hto, hts⟩ ht₂s t₂.independent.injective] at hc
exact (t₂.eq_circumradius_of_dist_eq hc h).symm
