centerMass_id_mem_convexHull_of_nonpos

English

Two equal centers of mass from same set with weights w yield the same mass as the center of mass of the combined weights.

Русский

Два одинаковых центра масс из одного множества и весов дают тот же центр массы, что и центр массы от суммарных весов.

LaTeX

$$centerMass\, w\, z = centerMass\, (a w) (b w) z$$

Lean4

/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive. -/
theorem centerMass_id_mem_convexHull_of_nonpos (t : Finset E) {w : E → R} (hw₀ : ∀ i ∈ t, w i ≤ 0)
    (hws : ∑ i ∈ t, w i < 0) : t.centerMass w id ∈ convexHull R (t : Set E) :=
  t.centerMass_mem_convexHull_of_nonpos hw₀ hws fun _ ↦ mem_coe.2

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