weightedVSub_map — Mathlib

English

If s2 is mapped along an embedding e, the weightedVSub over the image equals the weightedVSub over the preimage with composed weight and point maps.

Русский

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

LaTeX

$$$(s_2.map\, e).weightedVSub\ p\ w = s_2.weightedVSub\ (p\circ e)\ (w\circ e)$$$

Lean4

/-- A weighted subtraction, over the image of an embedding, equals a
weighted subtraction with the same points and weights over the
original `Finset`. -/
theorem weightedVSub_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
    (s₂.map e).weightedVSub p w = s₂.weightedVSub (p ∘ e) (w ∘ e) :=
  s₂.weightedVSubOfPoint_map _ _ _ _

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