Theorems · Definition · combinatorics

Multiset.map

{α : Type u_1} → {β : Type v} → (α → β) → Multiset α → Multiset β

map f s is the lift of the list map operation. The multiplicity of b in map f s is the number of a ∈ s (counting multiplicity) such that f a = b.

Defined in

Mathlib.Data.Multiset.MapFold

Cited by

876 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 43 definitions · uses propext, Quot.sound