centroid_univ — Mathlib

English

For a finite set s ⊆ P, the centroid of the inclusion map equals the centroid of s with the identity indexing: univ.centroid k (↑) = s.centroid k id.

Русский

Для конечного множества s ⊆ P центр масс включения равен центроиду множества s с идентичной индексацией: univ.centroid k (↑) = s.centroid k id.

LaTeX

$$$\\mathrm{centroid}(k,\\mathrm{univ},\\mathrm{Subtype.val}) = \\mathrm{centroid}(k,s,\\mathrm{id})$$$

Lean4

theorem centroid_univ (s : Finset P) : univ.centroid k ((↑) : s → P) = s.centroid k id :=
  by
  rw [centroid, centroid, ← s.attach_affineCombination_coe]
  congr
  ext
  simp

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