Theorems · Theorem · combinatorics

Multiset.map_pmap

∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (s : Multiset α)
  (H : ∀ a ∈ s, p a), Multiset.map g (Multiset.pmap f s H) = Multiset.pmap (fun a h => g (f a h)) s H

Defined in

Mathlib.Data.Multiset.MapFold

Cited by

7 results in Mathlib

Foundations

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