Documentation

Mathlib.Data.Multiset.Functor

Functoriality of Multiset. #

Equations
@[simp]
theorem Multiset.fmap_def {α' : Type u_1} {β' : Type u_1} {s : Multiset α'} (f : α'β') :
def Multiset.traverse {F : Type u → Type u} [Applicative F] [CommApplicative F] {α' : Type u} {β' : Type u} (f : α'F β') :
Multiset α'F (Multiset β')

Map each element of a Multiset to an action, evaluate these actions in order, and collect the results.

Equations
Instances For
    @[simp]
    theorem Multiset.pure_def {α : Type u_1} :
    pure = singleton
    @[simp]
    theorem Multiset.bind_def {α : Type u_1} {β : Type u_1} :
    (fun (x1 : Multiset α) (x2 : αMultiset β) => x1 >>= x2) = Multiset.bind
    @[simp]
    theorem Multiset.map_comp_coe {α : Type u_1} {β : Type u_1} (h : αβ) :
    Functor.map h Coe.coe = Coe.coe Functor.map h
    theorem Multiset.id_traverse {α : Type u_1} (x : Multiset α) :
    theorem Multiset.comp_traverse {G : Type u_1 → Type u_1} {H : Type u_1 → Type u_1} [Applicative G] [Applicative H] [CommApplicative G] [CommApplicative H] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : αG β) (h : βH γ) (x : Multiset α) :
    theorem Multiset.map_traverse {G : Type u_1 → Type u_1} [Applicative G] [CommApplicative G] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : αG β) (h : βγ) (x : Multiset α) :
    theorem Multiset.traverse_map {G : Type u_1 → Type u_1} [Applicative G] [CommApplicative G] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : αβ) (h : βG γ) (x : Multiset α) :
    theorem Multiset.naturality {G : Type u_1 → Type u_1} {H : Type u_1 → Type u_1} [Applicative G] [Applicative H] [CommApplicative G] [CommApplicative H] (eta : ApplicativeTransformation G H) {α : Type u_1} {β : Type u_1} (f : αG β) (x : Multiset α) :
    (fun {α : Type u_1} => eta.app α) (Multiset.traverse f x) = Multiset.traverse ((fun {α : Type u_1} => eta.app α) f) x