sum_centroidWeights_eq_one_of_cast_card_ne_zero

English

If the cardinality of s, cast to k, is nonzero, then the centroid weights sum to 1: ∑_{i∈s} s.centroidWeights(k,i) = 1 whenever (#s : k) ≠ 0.

Русский

Если число элементов s, приведённое в k, не нулевое, тогда веса центроида суммируются в 1: ∑_{i∈s} s.centroidWeights(k,i) = 1 при условии (#s : k) ≠ 0.

LaTeX

$$$\\#s \\neq 0 \\;\\Rightarrow\\; \\sum_{i\\in s} s.centroidWeights(k,i) = 1$$$

Lean4

/-- The weights in the centroid sum to 1, if the number of points,
converted to `k`, is not zero. -/
theorem sum_centroidWeights_eq_one_of_cast_card_ne_zero (h : (#s : k) ≠ 0) : ∑ i ∈ s, s.centroidWeights k i = 1 := by
  simp [h]

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