centroid_mem_affineSpan_of_card_eq_add_one

English

For CharZero k and s.Nonempty, the centroid lies in the affine span of range p: centroid ∈ affineSpan(k, range(p)).

Русский

Для CharZero k и s.Nonempty, центр масс лежит в афинном замке пространства: centroid ∈ affineSpan(k, range(p)).

LaTeX

$$$[CharZero\\ k] \\; \\{s: Finset\\ ι\\},\\; (p:\\ ι\\to P)\\Rightarrow s.centroid(k,p) \\in affineSpan(k, range(p))$$$

Lean4

/-- In the characteristic zero case, the centroid lies in the affine
span if the number of points is `n + 1`. -/
theorem centroid_mem_affineSpan_of_card_eq_add_one [CharZero k] {s : Finset ι} (p : ι → P) {n : ℕ} (h : #s = n + 1) :
    s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_card_eq_add_one k h) p

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