centroid_mem_affineSpan_of_nonempty

English

The definition of centroidWeightsIndicator is Set.indicator on s of s.centroidWeights k.

Русский

Определение centroidWeightsIndicator: индикатор множества s умноженный на веса центроида.

LaTeX

$$$s.centroidWeightsIndicator(k) = \\! Set.indicator(↑s)(s.centroidWeights(k))$$$

Lean4

/-- In the characteristic zero case, the centroid lies in the affine
span if the set is nonempty. -/
theorem centroid_mem_affineSpan_of_nonempty [CharZero k] {s : Finset ι} (p : ι → P) (h : s.Nonempty) :
    s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_nonempty k h) p

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