weightedVSubOfPoint_subtype_eq_filter

English

A weighted sum over a subtype equals the same weighted sum over the corresponding filtered set.

Русский

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

LaTeX

$$$ w:p \\mapsto ((s.subtype pred).weightedVSubOfPoint (p) b) = {x \\in s | pred x}.weightedVSubOfPoint p b w $$$

Lean4

/-- A weighted sum over `s.subtype pred` equals one over `{x ∈ s | pred x}`. -/
theorem weightedVSubOfPoint_subtype_eq_filter (w : ι → k) (p : ι → P) (b : P) (pred : ι → Prop) [DecidablePred pred] :
    ((s.subtype pred).weightedVSubOfPoint (fun i => p i) b fun i => w i) = {x ∈ s | pred x}.weightedVSubOfPoint p b w :=
  by rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]

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