Theorems · Definition · geometry

Affine.Simplex.mongePoint

{V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex ℝ P n → P

The Monge point of a simplex (in 2 or more dimensions) is a generalization of the orthocenter of a triangle. It is defined to be the intersection of the Monge planes, where a Monge plane is the (n-1)-dimensional affine subspace of the subspace spanned by the simplex that passes through the centroid of an (n-2)-dimensional face and is orthogonal to the opposite edge (in 2 dimensions, this is the same as an altitude). The circumcenter O, centroid G and Monge point M are collinear in that order on the Euler line, with OG : GM = (n-1): 2. Here, we use that ratio to define the Monge point (so resulting in a point that equals the centroid in 0 or 1 dimensions), and then show in subsequent lemmas that the point so defined lies in the Monge planes and is their unique point of intersection.

Defined in

Mathlib.Geometry.Euclidean.MongePoint

Cited by

20 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor