Theorems · Theorem · combinatorics

Multiset.countP_map

∀ {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) (p : β → Prop) [inst : DecidablePred p],
  Multiset.countP p (Multiset.map f s) = (Multiset.filter (fun a => p (f a)) s).card

Defined in

Mathlib.Data.Multiset.Filter

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidablePred