Theorems · Definition · combinatorics

Multiset.pmap

{α : Type u_1} → {β : Type v} → {p : α → Prop} → ((a : α) → p a → β) → (s : Multiset α) → (∀ a ∈ s, p a) → Multiset β

Lift of the list pmap operation. Map a partial function f over a multiset s whose elements are all in the domain of f.

Defined in

Mathlib.Data.Multiset.Defs

Cited by

16 results in Mathlib

Foundations

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