mathlib documentation

data.multiset.functor

Functoriality of multiset.

@[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 β')multiset α'F (multiset β')

Equations
@[instance]

Equations
@[simp]
theorem multiset.pure_def {α : Type u_1} :
pure = λ (x : α), x ::ₘ 0

@[simp]
theorem multiset.bind_def {α β : Type u_1} :

@[simp]
theorem multiset.lift_beta {α : 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 α) :