English
The sum of mongePointVSubFaceCentroidWeightsWithCircumcenter over all i equals zero when subtracting the centroid weights from mongePointWeightsWithCircumcenter.
Русский
Сумма весов mongePointVSubFaceCentroidWeightsWithCircumcenter по всем i равна нулю, когда вычитаются веса центра монге.
LaTeX
$$$$ \sum_i mongePointVSubFaceCentroidWeightsWithCircumcenter i_1 i_2 i = 0. $$$$
Lean4
/-- The Monge point of an (n+2)-simplex, minus the centroid of an
n-dimensional face, in terms of `pointsWithCircumcenter`. -/
theorem mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P (n + 2))
{i₁ i₂ : Fin (n + 3)} (h : i₁ ≠ i₂) :
s.mongePoint -ᵥ ({ i₁, i₂ }ᶜ : Finset (Fin (n + 3))).centroid ℝ s.points =
(univ : Finset (PointsWithCircumcenterIndex (n + 2))).weightedVSub s.pointsWithCircumcenter
(mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂) :=
by
simp_rw [mongePoint_eq_affineCombination_of_pointsWithCircumcenter,
centroid_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_vsub,
mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub h]
