centroid_eq_centerMass — Mathlib

English

The centroid can be identified with the center of mass using centroid weights.

Русский

Центроид можно идентифицировать как центр массы, используя веса центроида.

LaTeX

$$centroid R s p = centerMass R (s.centroidWeights R) p$$

Lean4

/-- The centroid can be regarded as a center of mass. -/
@[simp]
theorem centroid_eq_centerMass (s : Finset ι) (hs : s.Nonempty) (p : ι → E) :
    s.centroid R p = s.centerMass (s.centroidWeights R) p :=
  affineCombination_eq_centerMass (s.sum_centroidWeights_eq_one_of_nonempty R hs)

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