Theorems · Theorem · combinatorics

Finset.fold_disjSum

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (t : Finset β) (f : α ⊕ β → γ) (b₁ b₂ : γ)
  (op : γ → γ → γ) [inst : Std.Commutative op] [inst_1 : Std.Associative op],
  Finset.fold op (op b₁ b₂) f (s.disjSum t) =
    op (Finset.fold op b₁ (fun x => f (Sum.inl x)) s) (Finset.fold op b₂ (fun x => f (Sum.inr x)) t)

Defined in

Mathlib.Data.Finset.Sum

Cited by

2 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.Associative