weightedVSub_indicator_subset — Mathlib

English

Replacing weights by an indicator of a subset, while expanding the index set, does not change the result of WeightedVSub when the subset relation holds.

Русский

Замена весов на индикатор подмножества и расширение индекса не меняют WeightedVSub при условии включения.

LaTeX

$$$s_1\subseteq s_2 \Rightarrow s_1.weightedVSub(p,w)=s_2.weightedVSub(p,\mathrm{indicator}(\uparrow s_1)\, w)$$$

Lean4

/-- The weighted sum is unaffected by changing the weights to the
corresponding indicator function and adding points to the set. -/
theorem weightedVSub_indicator_subset (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
    s₁.weightedVSub p w = s₂.weightedVSub p (Set.indicator (↑s₁) w) :=
  weightedVSubOfPoint_indicator_subset _ _ _ h

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