Theorems · Theorem · combinatorics

Multiset.filter_cons

∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
  Multiset.filter p (a ::ₘ s) = (if p a then {a} else 0) + Multiset.filter p s

Defined in

Mathlib.Data.Multiset.Filter

Cited by

5 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

DecidablePred