Theorems · Theorem · combinatorics

Multiset.filterMap_cons

∀ {α : Type u_1} {β : Type v} (f : α → Option β) (a : α) (s : Multiset α),
  Multiset.filterMap f (a ::ₘ s) = (Option.map singleton (f a)).getD 0 + Multiset.filterMap f s

Defined in

Mathlib.Data.Multiset.Filter

Cited by

2 results in Mathlib

Foundations

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