English
For an orthocentric system, any triple of pairwise distinct points is affinely independent.
Русский
Для ортокцентрической системы любая тройка попарно различных точек афинно независима.
LaTeX
$$$\text{AffineIndependent}(\_\_)$$$
Lean4
/-- For any three points in an orthocentric system generated by
triangle `t`, there is a point in the subspace spanned by the triangle
from which the distance of all those three points equals the circumradius. -/
theorem exists_dist_eq_circumradius_of_subset_insert_orthocenter {t : Triangle ℝ P}
(ho : t.orthocenter ∉ Set.range t.points) {p : Fin 3 → P}
(hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)) (hpi : Function.Injective p) :
∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = t.circumradius :=
by
rcases exists_of_range_subset_orthocentricSystem ho hps hpi with
(⟨i₁, i₂, i₃, j₂, j₃, _, _, _, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩ | hs)
· use reflection (affineSpan ℝ (t.points '' { j₂, j₃ })) t.circumcenter,
reflection_mem_of_le_of_mem (affineSpan_mono ℝ (Set.image_subset_range _ _)) t.circumcenter_mem_affineSpan
intro p₁ hp₁
rcases hp₁ with ⟨i, rfl⟩
have h₁₂₃ := h₁₂₃ i
repeat' rcases h₁₂₃ with h₁₂₃ | h₁₂₃
· convert Triangle.dist_orthocenter_reflection_circumcenter t hj₂₃
· rw [← h₂, dist_reflection_eq_of_mem _ (mem_affineSpan ℝ (Set.mem_image_of_mem _ (Set.mem_insert _ _)))]
exact t.dist_circumcenter_eq_circumradius _
· rw [← h₃,
dist_reflection_eq_of_mem _
(mem_affineSpan ℝ (Set.mem_image_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))]
exact t.dist_circumcenter_eq_circumradius _
· use t.circumcenter, t.circumcenter_mem_affineSpan
intro p₁ hp₁
rw [hs] at hp₁
rcases hp₁ with ⟨i, rfl⟩
exact t.dist_circumcenter_eq_circumradius _
