Theorems · Theorem · combinatorics

Finset.fold_insert

∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {a : α} [inst : DecidableEq α],
  a ∉ s → Finset.fold op b f (insert a s) = op (f a) (Finset.fold op b f s)

Defined in

Mathlib.Data.Finset.Fold

Cited by

11 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.AssociativeDecidableEq