orthocenter_eq_of_range_eq — Mathlib

English

If two triangles have exactly the same set of vertices, their orthocenters coincide.

Русский

Если два треугольника имеют одинаковый набор вершин, их ортоцентр совпадает.

LaTeX

$$$\forall t_1,t_2,\ (\operatorname{range}t_1.points = \operatorname{range}t_2.points) \Rightarrow t_1.\text{orthocenter} = t_2.\text{orthocenter}$$$

Lean4

/-- Two triangles with the same points have the same orthocenter. -/
theorem orthocenter_eq_of_range_eq {t₁ t₂ : Triangle ℝ P} (h : Set.range t₁.points = Set.range t₂.points) :
    t₁.orthocenter = t₂.orthocenter :=
  mongePoint_eq_of_range_eq h

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