centroid_map — Mathlib

English

If p is injective on s and p''↑s = p''↑s₂, then the centroid of s with p equals the centroid of s₂ with p₂ evaluated consistently via the image.

Русский

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

LaTeX

$$$s.\\mathrm{centroid}(k,p) = s_2.\\mathrm{centroid}(k,p_2)$ при соответствии образов через p'$$

Lean4

/-- A centroid, over the image of an embedding, equals a centroid with
the same points and weights over the original `Finset`. -/
theorem centroid_map (e : ι₂ ↪ ι) (p : ι → P) : (s₂.map e).centroid k p = s₂.centroid k (p ∘ e) := by
  simp [centroid_def, affineCombination_map, centroidWeights]

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