Theorems · Theorem · order theory

sum_collapse

∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] {𝒜 : Finset (Finset α)} {a : α}
  {f : Finset α → β} {u : Finset α},
  𝒜 ⊆ (insert a u).powerset → a ∉ u → ∑ s ∈ u.powerset, collapse✝ 𝒜 a f s = ∑ s ∈ 𝒜, f s

Defined in

Mathlib.Combinatorics.SetFamily.FourFunctions

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqCommSemiring