centroidWeights_apply

Mathlib.LinearAlgebra.AffineSpace.Centroid

URI: https://scilib.ai/kg/mathlib#Finset.centroidWeights_apply

English

For any k, ι, and finite s, the centroid weights satisfy centroidWeights k s i = (#s)^{-1}.

Русский

Для любых k, ι и конечного s веса центроида удовлетворяют centroidWeights k s i = (#s)^{-1}.

LaTeX

$$$ s.\\text{centroidWeights } k\\; i = (#s : k)^{-1}$$$

Lean4

/-- `centroidWeights` at any point. -/
@[simp]
theorem centroidWeights_apply (i : ι) : s.centroidWeights k i = (#s : k)⁻¹ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru