# mathlibdocumentation

data.multiset.functor

# Functoriality of multiset. #

@[protected, instance]
Equations
@[simp]
theorem multiset.fmap_def {α' β' : Type u_1} {s : multiset α'} (f : α' → β') :
f <\$> s = s
@[protected, instance]
def multiset.traverse {F : Type uType u} [applicative F] {α' β' : Type u} (f : α' → F β') :
multiset α'F (multiset β')
Equations
@[protected, instance]
Equations
@[simp]
theorem multiset.pure_def {α : Type u_1} :
@[simp]
theorem multiset.bind_def {α β : Type u_1} :
@[protected, instance]
@[simp]
theorem multiset.lift_coe {α : Type u_1} {β : Type u_2} (x : list α) (f : list α → β) (h : ∀ (a b : list α), a bf a = f b) :
x = f x
@[simp]
theorem multiset.map_comp_coe {α β : Type u_1} (h : α → β) :
=
theorem multiset.id_traverse {α : Type u_1} (x : multiset α) :
theorem multiset.comp_traverse {G H : Type u_1Type u_1} [applicative G] [applicative H] {α β γ : Type u_1} (g : α → G β) (h : β → H γ) (x : multiset α) :
theorem multiset.map_traverse {G : Type u_1Type u_1} [applicative G] {α β γ : Type u_1} (g : α → G β) (h : β → γ) (x : multiset α) :
= x
theorem multiset.traverse_map {G : Type u_1Type u_1} [applicative G] {α β γ : Type u_1} (g : α → β) (h : β → G γ) (x : multiset α) :
x) = multiset.traverse (h g) x
theorem multiset.naturality {G H : Type u_1Type u_1} [applicative G] [applicative H] (eta : H) {α β : Type u_1} (f : α → G β) (x : multiset α) :
eta x) = multiset.traverse (eta f) x