Theorems · Definition · geometry

EuclideanGeometry.OrthocentricSystem

{V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] → [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → Set P → Prop

Four points form an orthocentric system if they consist of the vertices of a triangle and its orthocenter.

Defined in

Mathlib.Geometry.Euclidean.MongePoint

Cited by

4 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor