Theorems · Theorem · order theory

collapse_eq

∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] {a : α} {s : Finset α},
  a ∉ s →
    ∀ (𝒜 : Finset (Finset α)) (f : Finset α → β),
      collapse✝ 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0

Defined in

Mathlib.Combinatorics.SetFamily.FourFunctions

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEqCommSemiring