centroid_mem_affineSpan_of_card_ne_zero

English

The centroidWeightsIndicator is defined as Set.indicator(↑s)(s.centroidWeights k).

Русский

centroidWeightsIndicator определяется как Set.indicator(↑s)(s.centroidWeights k).

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 number of points is not zero. -/
theorem centroid_mem_affineSpan_of_card_ne_zero [CharZero k] {s : Finset ι} (p : ι → P) (h : #s ≠ 0) :
    s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_card_ne_zero k h) p

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