English
In an orthocentric system, the fourth point is the orthocenter of any triangle lying in the system; hence the system equals the union of the triangle's three points with its orthocenter.
Русский
В ортокцентрической системе четвертая точка является ортоцентрoм любой треугольной главы системы; следовательно, система равна объединению трёх вершин треугольника и его ортоцентра.
LaTeX
$$$s = \\operatorname{insert}(t.orthocenter, \\mathrm{range}(t.points))$$$
Lean4
/-- Given any triangle in an orthocentric system, the fourth point is
its orthocenter. -/
theorem eq_insert_orthocenter {s : Set P} (ho : OrthocentricSystem s) {t : Triangle ℝ P} (ht : Set.range t.points ⊆ s) :
s = insert t.orthocenter (Set.range t.points) :=
by
rcases ho with ⟨t₀, ht₀o, ht₀s⟩
rw [ht₀s] at ht
rcases exists_of_range_subset_orthocentricSystem ht₀o ht t.independent.injective with
(⟨i₁, i₂, i₃, j₂, j₃, h₁₂, h₁₃, h₂₃, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩ | hs)
· obtain ⟨j₁, hj₁₂, hj₁₃, hj₁₂₃⟩ : ∃ j₁ : Fin 3, j₁ ≠ j₂ ∧ j₁ ≠ j₃ ∧ ∀ j : Fin 3, j = j₁ ∨ j = j₂ ∨ j = j₃ :=
by
clear h₂ h₃
decide +revert
suffices h : t₀.points j₁ = t.orthocenter
by
have hui : (Set.univ : Set (Fin 3)) = { i₁, i₂, i₃ } := by ext x; simpa using h₁₂₃ x
have huj : (Set.univ : Set (Fin 3)) = { j₁, j₂, j₃ } := by ext x; simpa using hj₁₂₃ x
rw [← h, ht₀s, ← Set.image_univ, huj, ← Set.image_univ, hui]
simp_rw [Set.image_insert_eq, Set.image_singleton, h₁, ← h₂, ← h₃]
rw [Set.insert_comm]
exact (Triangle.orthocenter_replace_orthocenter_eq_point hj₁₂ hj₁₃ hj₂₃ h₁₂ h₁₃ h₂₃ h₁ h₂.symm h₃.symm).symm
· rw [hs]
convert ht₀s using 2
exact Triangle.orthocenter_eq_of_range_eq hs
