Theorems · Theorem · combinatorics

Finset.fold_ite

∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} [Std.IdempotentOp op] {g : α → β} (p : α → Prop) [inst : DecidablePred p],
  Finset.fold op b (fun i => if p i then f i else g i) s =
    op (Finset.fold op b f (Finset.filter p s)) (Finset.fold op b g ({i ∈ s | ¬p i}))

A weaker version of Finset.fold_ite', relying on typeclass idempotency over the whole type, instead of solely on the seed element. However, this is easier to use because it does not generate side goals.

Defined in

Mathlib.Data.Finset.Fold

Cited by

3 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.AssociativeStd.IdempotentOpDecidablePred