sum_fiberwise — Mathlib

English

Sum over fibers: summing g over all J in π.boxes, grouped by f(J) labels, equals the total sum over π.boxes.

Русский

Суммирование по фибрам: сумма g по всем J в π.boxes, сгруппированная по значениям f(J), равна полной сумме по π.boxes.

LaTeX

$$$ \sum_{y \in π.boxes.image f} \; \sum_{J \in (π.filter (\ lambda J, f J = y)).boxes} g(J) \;=\; \sum_{J \in π.boxes} g(J). $$$

Lean4

theorem sum_fiberwise {α M} [AddCommMonoid M] (π : Prepartition I) (f : Box ι → α) (g : Box ι → M) :
    (∑ y ∈ π.boxes.image f, ∑ J ∈ (π.filter fun J => f J = y).boxes, g J) = ∑ J ∈ π.boxes, g J := by
  convert sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g

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