weightedVSub_filter_of_ne — Mathlib

English

If all nonzero weights in s outside pred are zero, then the weightedVSub over the filtered set equals the whole-set weightedVSub.

Русский

Если все ненулевые веса не удовлетворяют pred, то взвешенная сумма по фильтрованному набору равна полной weightedVSub.

LaTeX

$$$(\mathrm{Set}.indicator(↑s|pred) w) = w$ подмножество;\; {x\in s\;|\; pred x}.weightedVSub p w = s.weightedVSub p w$$$

Lean4

/-- A weighted sum over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices in `s`
not satisfying `pred` are zero. -/
theorem weightedVSub_filter_of_ne (w : ι → k) (p : ι → P) {pred : ι → Prop} [DecidablePred pred]
    (h : ∀ i ∈ s, w i ≠ 0 → pred i) : {x ∈ s | pred x}.weightedVSub p w = s.weightedVSub p w :=
  s.weightedVSubOfPoint_filter_of_ne _ _ _ h

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