Theorems · Theorem · order theory

Finpartition.sum_restrict

∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hb : b ≤ a) {M : Type u_2} [inst_3 : AddCommMonoid M] (f : α → M),
  f ⊥ = 0 → ∑ p ∈ (P.restrict hb).parts, f p = ∑ q ∈ P.parts, f (q ⊓ b)

The sum of a set-valued function over restricted partition parts equals the sum over original parts with f (· ⊓ b), provided f ⊥ = 0 (so bottom terms don't contribute).

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

DistribLatticeOrderBotDecidableEqAddCommMonoid