Theorems · Theorem · order theory

Finpartition.sum_combine

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {ι : Type u_2} {I : Finset ι} {s : ι → α} (P : (i : ι) → Finpartition (s i)) (ha : I.SupIndep s) {M : Type u_3}
  [inst_4 : AddCommMonoid M] (f : α → M), ∑ p ∈ (Finpartition.combine P ha).parts, f p = ∑ i ∈ I, ∑ p ∈ (P i).parts, f p

The sum of a set-valued function over a combined partition equals the sum of sums over component partitions.

Defined in

Mathlib.Order.Partition.Finpartition

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LatticeOrderBotIsModularLatticeDecidableEqAddCommMonoid