OrthocentricSystem — Mathlib

English

A set of four points forms an orthocentric system if it consists of the vertices of a triangle and its orthocenter.

Русский

Множество из четырёх точек образует ортокоцентрическую систему, если оно состоит из вершин треугольника и его ортоцентра.

LaTeX

$$def OrthocentricSystem (s : Set P) : Prop := ∃ t : Triangle ℝ P, t.orthocenter ∉ Set.range t.points ∧ s = insert t.orthocenter (Set.range t.points)$$

Lean4

/-- Four points form an orthocentric system if they consist of the
vertices of a triangle and its orthocenter. -/
def OrthocentricSystem (s : Set P) : Prop :=
  ∃ t : Triangle ℝ P, t.orthocenter ∉ Set.range t.points ∧ s = insert t.orthocenter (Set.range t.points)

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