centroid_mem_affineSpan_of_cast_card_ne_zero

English

If p and p2 are injective on s and s2 and p''↑s = p2''↑s2, then centroids agree.

Русский

Если p и p2 инъективны на s и s2 и образы совпадают, то центроиды равны.

LaTeX

$$$\\forall p:\\ ι→P,\\; hi:\\; \\text{inj on } s, \\; \\forall p_2:\\ ι_2→P, hi_2:\\; \\text{inj on } s_2, \\; (he:\\ p '' ↑s = p_2 '' ↑s_2) \\Rightarrow s.centroid k p = s_2.centroid k p_2$$$

Lean4

/-- The centroid lies in the affine span if the number of points,
converted to `k`, is not zero. -/
theorem centroid_mem_affineSpan_of_cast_card_ne_zero {s : Finset ι} (p : ι → P) (h : (#s : k) ≠ 0) :
    s.centroid k p ∈ affineSpan k (range p) :=
  affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_cast_card_ne_zero h) p

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