mongePoint_eq_smul_vsub_vadd_circumcenter

English

For an (n+2)-simplex s, the Monge point M, the circumcenter O, and the centroid G are collinear with OG:GM = (n−1):2; equivalently, M lies on the Euler line through O and G with that ratio.

Русский

У (n+2)-многоугольника MongePoint M, центр описанной окружности O и центроид G лежат на одной прямой (Euler line) в отношении OG:GM = (n−1):2.

LaTeX

$$$$ M = O + \frac{n+1}{n-1}\,(G - O). $$$$

Lean4

/-- The position of the Monge point in relation to the circumcenter
and centroid. -/
theorem mongePoint_eq_smul_vsub_vadd_circumcenter {n : ℕ} (s : Simplex ℝ P n) :
    s.mongePoint =
      (((n + 1 : ℕ) : ℝ) / ((n - 1 : ℕ) : ℝ)) • ((univ : Finset (Fin (n + 1))).centroid ℝ s.points -ᵥ s.circumcenter) +ᵥ
        s.circumcenter :=
  rfl

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