English
If a point lies on two distinct altitudes of a triangle, it must be the orthocenter.
Русский
Если точка лежит на двух разных высотах треугольника, то она является ортоцентрeм.
LaTeX
$$$\text{If } p\in t.\text{altitude}_{i_1}\cap t.\text{altitude}_{i_2}\text{ with } i_1\neq i_2, \text{ then } p=t.\text{orthocenter}.$$$
Lean4
/-- In the case of a triangle, altitudes are the same thing as Monge
planes. -/
theorem altitude_eq_mongePlane (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
t.altitude i₁ = t.mongePlane i₂ i₃ :=
by
have hs : ({ i₂, i₃ }ᶜ : Finset (Fin 3)) = { i₁ } := by decide +revert
have he : ({ i₁ }ᶜ : Set (Fin 3)) = { i₂, i₃ } := by ext; decide +revert
rw [mongePlane_def, altitude_def, direction_affineSpan, hs, he, centroid_singleton,
vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_insert i₂ _)]
simp [h₂₃]
