centerMass_mem_convexHull_of_nonpos

English

The center of mass of a finite mix of vectors equals the finite convex combination of those vectors with the given weights.

Русский

Центр массы конечной смеси векторов равен их конечной выпуклой комбинации с заданными весами.

LaTeX

$$t.centerMass w z ∈ E$$

Lean4

/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive. -/
theorem centerMass_mem_convexHull_of_nonpos (t : Finset ι) (hw₀ : ∀ i ∈ t, w i ≤ 0) (hws : ∑ i ∈ t, w i < 0)
    (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass w z ∈ convexHull R s :=
  by
  rw [← centerMass_neg_left]
  exact Finset.centerMass_mem_convexHull _ (fun _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz

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