weightedVSub_subtype_eq_filter — Mathlib

English

A weighted sum over a subtype equals the weighted sum over the original set after appropriate reinterpretation of indices (subtype s.pred).

Русский

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

LaTeX

$$$((s\text{.subtype } pred).weightedVSub (p\circ i) (w\circ i)) = {x\in s\;|\; pred x}.weightedVSub p w$$$

Lean4

/-- A weighted sum over `s.subtype pred` equals one over `{x ∈ s | pred x}`. -/
theorem weightedVSub_subtype_eq_filter (w : ι → k) (p : ι → P) (pred : ι → Prop) [DecidablePred pred] :
    ((s.subtype pred).weightedVSub (fun i => p i) fun i => w i) = {x ∈ s | pred x}.weightedVSub p w :=
  s.weightedVSubOfPoint_subtype_eq_filter _ _ _ _

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