Theorems · Theorem · combinatorics

Finset.fold_disjUnion

∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
  {s₁ s₂ : Finset α} {b₁ b₂ : β} (h : Disjoint s₁ s₂),
  Finset.fold op (op b₁ b₂) f (s₁.disjUnion s₂ h) = op (Finset.fold op b₁ f s₁) (Finset.fold op b₂ f s₂)

Defined in

Mathlib.Data.Finset.Fold

Cited by

2 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.Associative