centerMass_mem_convexHull — Mathlib

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

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