English
A weighted sum over the image of an embedding equals the sum over the original set with composed p and w.
Русский
Взвешенная сумма по образу вложения равна сумме по исходному множеству с композициями p и w.
LaTeX
$$$ (s_2.map e).weightedVSubOfPoint p b w = s_2.weightedVSubOfPoint (p \\circ e) b (w \\circ e) $$$
Lean4
/-- Applying `weightedVSub` with given weights. This is for the case
where a result involving a default base point is OK (for example, when
that base point will cancel out later); a more typical use case for
`weightedVSub` would involve selecting a preferred base point with
`weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero` and then
using `weightedVSubOfPoint_apply`. -/
theorem weightedVSub_apply (w : ι → k) (p : ι → P) :
s.weightedVSub p w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice S.nonempty) := by simp [weightedVSub]
