orthocenter_mem_altitude — Mathlib

English

The orthocenter lies on any altitude from a vertex of the triangle.

Русский

Ортогцентр лежит на любой высоте треугольника, исходящей от вершины.

LaTeX

$$$t.\text{orthocenter} \in t.\text{altitude}_{i}$ for any i ∈ Fin 3.$$

Lean4

/-- The orthocenter lies in the altitudes. -/
theorem orthocenter_mem_altitude (t : Triangle ℝ P) {i₁ : Fin 3} : t.orthocenter ∈ t.altitude i₁ :=
  by
  obtain ⟨i₂, i₃, h₁₂, h₂₃, h₁₃⟩ : ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by decide +revert
  rw [orthocenter_eq_mongePoint, t.altitude_eq_mongePlane h₁₂ h₁₃ h₂₃]
  exact t.mongePoint_mem_mongePlane

Похожие утверждения