English
Any three points in an orthocentric system are affinely independent.
Русский
Любые три точки в ортокцентрической системе афинно независимы.
LaTeX
$$Theorem: OrthocentricSystem.affineIndependent$$
Lean4
/-- This is an auxiliary lemma giving information about the relation
of two triangles in an orthocentric system; it abstracts some
reasoning, with no geometric content, that is common to some other
lemmas. Suppose the orthocentric system is generated by triangle `t`,
and we are given three points `p` in the orthocentric system. Then
either we can find indices `i₁`, `i₂` and `i₃` for `p` such that `p
i₁` is the orthocenter of `t` and `p i₂` and `p i₃` are points `j₂`
and `j₃` of `t`, or `p` has the same points as `t`. -/
theorem exists_of_range_subset_orthocentricSystem {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) :
(∃ i₁ i₂ i₃ j₂ j₃ : Fin 3,
i₁ ≠ i₂ ∧
i₁ ≠ i₃ ∧
i₂ ≠ i₃ ∧
(∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
Set.range p = Set.range t.points :=
by
by_cases h : t.orthocenter ∈ Set.range p
· left
rcases h with ⟨i₁, h₁⟩
obtain ⟨i₂, i₃, h₁₂, h₁₃, h₂₃, h₁₂₃⟩ :
∃ i₂ i₃ : Fin 3, i₁ ≠ i₂ ∧ i₁ ≠ i₃ ∧ i₂ ≠ i₃ ∧ ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ :=
by
clear h₁
decide +revert
have h : ∀ i, i₁ ≠ i → ∃ j : Fin 3, t.points j = p i :=
by
intro i hi
replace hps :=
Set.mem_of_mem_insert_of_ne (Set.mem_of_mem_of_subset (Set.mem_range_self i) hps) (h₁ ▸ hpi.ne hi.symm)
exact hps
rcases h i₂ h₁₂ with ⟨j₂, h₂⟩
rcases h i₃ h₁₃ with ⟨j₃, h₃⟩
have hj₂₃ : j₂ ≠ j₃ := by
intro he
rw [he, h₃] at h₂
exact h₂₃.symm (hpi h₂)
exact ⟨i₁, i₂, i₃, j₂, j₃, h₁₂, h₁₃, h₂₃, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩
· right
have hs := Set.subset_diff_singleton hps h
rw [Set.insert_diff_self_of_notMem ho] at hs
classical
refine Set.eq_of_subset_of_card_le hs ?_
rw [Set.card_range_of_injective hpi, Set.card_range_of_injective t.independent.injective]
