Theorems · Theorem · combinatorics

Multiset.countP_cons

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

Defined in

Mathlib.Data.Multiset.Count

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidablePred