Theorems · Theorem · combinatorics

Finset.fold_union_inter

∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
  [inst : DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : β},
  op (Finset.fold op b₁ f (s₁ ∪ s₂)) (Finset.fold op b₂ f (s₁ ∩ s₂)) =
    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.AssociativeDecidableEq