weightedVSubOfPoint_map — Mathlib

English

A weighted sum over the image of an embedding equals the same weighted sum over the original index set, with the index and weight functions composed with the embedding.

Русский

Взвешенная сумма по образу вложения равна той же сумме по исходному индексу с композициями функций.

LaTeX

$$$ (s_2.map e).weightedVSubOfPoint p b w = s_2.weightedVSubOfPoint (p \\circ e) b (w \\circ e) $$$

Lean4

/-- A weighted sum, over the image of an embedding, equals a weighted
sum with the same points and weights over the original
`Finset`. -/
theorem weightedVSubOfPoint_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P) :
    (s₂.map e).weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint (p ∘ e) b (w ∘ e) :=
  by
  simp_rw [weightedVSubOfPoint_apply]
  exact Finset.sum_map _ _ _

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