English
Centroid is a special case of an affine combination of masses, giving the centroid as a center of mass with centroid weights.
Русский
Центроид является частным случаем аффинной комбинации масс; центроид — центр массы с весами центроида.
LaTeX
$$s.centroid R p = s.centerMass (s.centroidWeights R) p$$
Lean4
theorem centerMass_mem_convexHull (t : Finset ι) {w : ι → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < ∑ i ∈ t, w i)
{z : ι → E} (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass w z ∈ convexHull R s :=
(convex_convexHull R s).centerMass_mem hw₀ hws fun i hi => subset_convexHull R s <| hz i hi