English
For an (n+2)-simplex s, the Monge point M can be expressed as an affine combination of the pointsWithCircumcenter with weights mongePointWeightsWithCircumcenter n.
Русский
Для (n+2)-многоугольника s MongePoint можно выразить как аффинную комбинацию точекWithCircumcenter со весами mongePointWeightsWithCircumcenter n.
LaTeX
$$$$ s.mongePoint = (univ : Finset (PointsWithCircumcenterIndex (n+2))).affineCombination \mathbb{R} \bigl(s.pointsWithCircumcenter\bigr) (mongePointWeightsWithCircumcenter n). $$$$
Lean4
/-- Two simplices with the same points have the same Monge point. -/
theorem mongePoint_eq_of_range_eq {n : ℕ} {s₁ s₂ : Simplex ℝ P n} (h : Set.range s₁.points = Set.range s₂.points) :
s₁.mongePoint = s₂.mongePoint := by
simp_rw [mongePoint_eq_smul_vsub_vadd_circumcenter, centroid_eq_of_range_eq h, circumcenter_eq_of_range_eq h]
