Theorems · Theorem · combinatorics

Finset.fold_disjiUnion

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {ι : Type u_4} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h : (↑s).PairwiseDisjoint t),
  Finset.fold op (Finset.fold op b₀ b s) f (s.disjiUnion t h) =
    Finset.fold op b₀ (fun i => Finset.fold op (b i) f (t i)) s

Defined in

Mathlib.Data.Finset.Union

Cited by

2 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.Associative