mathlib3 documentation

data.multiset.functor

Functoriality of multiset. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def multiset.functor  :
functor multiset
Equations
source
@[simp]
theorem multiset.fmap_def {α' β' : Type u_1} {s : multiset α'} (f : α' → β') :
f <$> s = multiset.map f s
source
@[protected, instance]
def multiset.is_lawful_functor  :
is_lawful_functor multiset
source
def multiset.traverse {F : Type u → Type u} [applicative F] [is_comm_applicative F] {α' β' : Type u} (f : α' → F β') :
multiset α' → F (multiset β')
Equations
source
@[protected, instance]
def multiset.monad  :
monad multiset
Equations
source
@[simp]
theorem multiset.pure_def {α : Type u_1} :
has_pure.pure = has_singleton.singleton
source
@[simp]
theorem multiset.bind_def {α β : Type u_1} :
has_bind.bind = multiset.bind
source
@[protected, instance]
def multiset.is_lawful_monad  :
is_lawful_monad multiset
source
@[simp]
theorem multiset.lift_coe {α : Type u_1} {β : Type u_2} (x : list α) (f : list α → β) (h : ∀ (a b : list α), a ≈ b → f a = f b) :
quotient.lift f h ↑x = f x
source
@[simp]
theorem multiset.map_comp_coe {α β : Type u_1} (h : α → β) :
functor.map h ∘ coe = coe ∘ functor.map h
source
theorem multiset.id_traverse {α : Type u_1} (x : multiset α) :
multiset.traverse id.mk x = x
source
theorem multiset.comp_traverse {G H : Type u_1 → Type u_1} [applicative G] [applicative H] [is_comm_applicative G] [is_comm_applicative H] {α β γ : Type u_1} (g : α → G β) (h : β → H γ) (x : multiset α) :
multiset.traverse (functor.comp.mk ∘ functor.map h ∘ g) x = functor.comp.mk (multiset.traverse h <$> multiset.traverse g x)
source
theorem multiset.map_traverse {G : Type u_1 → Type u_1} [applicative G] [is_comm_applicative G] {α β γ : Type u_1} (g : α → G β) (h : β → γ) (x : multiset α) :
functor.map h <$> multiset.traverse g x = multiset.traverse (functor.map h ∘ g) x
source
theorem multiset.traverse_map {G : Type u_1 → Type u_1} [applicative G] [is_comm_applicative G] {α β γ : Type u_1} (g : α → β) (h : β → G γ) (x : multiset α) :
multiset.traverse h (multiset.map g x) = multiset.traverse (h ∘ g) x
source
theorem multiset.naturality {G H : Type u_1 → Type 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 α) :
⇑eta (multiset.traverse f x) = multiset.traverse (⇑eta ∘ f) x