centerMass_id_mem_convexHull — Mathlib

English

The center mass of a pair of finite index sets is the center mass of the union with the induced weights and points.

Русский

Центр массы пары конечных множеств равен центру массы их объединения с соответствующими весами и точками.

LaTeX

$$s.centerMass w z + t.centerMass w z = (s.disjSum t).centerMass (Sum.elim ...) (Sum.elim zs zt)$$

Lean4

/-- A refinement of `Finset.centerMass_mem_convexHull` when the indexed family is a `Finset` of
the space. -/
theorem centerMass_id_mem_convexHull (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < ∑ i ∈ t, w i) :
    t.centerMass w id ∈ convexHull R (t : Set E) :=
  t.centerMass_mem_convexHull hw₀ hws fun _ => mem_coe.2

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