mathlib documentation

data.multiset.functor

Functoriality of multiset. #

@[protected, instance]
Equations
@[simp]
theorem multiset.fmap_def {α' β' : Type u_1} {s : multiset α'} (f : α' → β') :
def multiset.traverse {F : Type uType u} [applicative F] [is_comm_applicative F] {α' β' : Type u} (f : α' → F β') :
multiset α'F (multiset β')
Equations
@[protected, instance]
Equations
@[simp]
@[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) :
@[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] [is_comm_applicative G] [is_comm_applicative H] {α β γ : Type u_1} (g : α → G β) (h : β → H γ) (x : multiset α) :
theorem multiset.map_traverse {G : Type u_1Type u_1} [applicative G] [is_comm_applicative G] {α β γ : Type u_1} (g : α → G β) (h : β → γ) (x : multiset α) :
theorem multiset.traverse_map {G : Type u_1Type u_1} [applicative G] [is_comm_applicative G] {α β γ : Type u_1} (g : α → β) (h : β → G γ) (x : multiset α) :
theorem multiset.naturality {G H : Type u_1Type u_1} [applicative G] [applicative H] [is_comm_applicative G] [is_comm_applicative H] (eta : applicative_transformation G H) {α β : Type u_1} (f : α → G β) (x : multiset α) :