Theorems · Theorem · combinatorics

Multiset.sub_filter_eq_filter_not

∀ {α : Type u_1} [inst : DecidableEq α] (p : α → Prop) [inst_1 : DecidablePred p] (s : Multiset α),
  s - Multiset.filter p s = Multiset.filter (fun a => ¬p a) s

Defined in

Mathlib.Data.Multiset.Filter

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidablePred