# Documentation

Mathlib.Data.Finset.Functor

# Functoriality of Finset#

This file defines the functor structure of Finset.

## TODO #

Currently, all instances are classical because the functor classes want to run over all types. If instead we could state that a functor is lawful/applicative/traversable... between two given types, then we could provide the instances for types with decidable equality.

### Functor #

instance Finset.functor [(P : Prop) → ] :

Because Finset.image requires a DecidableEq instance for the target type, we can only construct Functor Finset when working classically.

instance Finset.lawfulFunctor [(P : Prop) → ] :
@[simp]
theorem Finset.fmap_def {α : Type u} {β : Type u} [(P : Prop) → ] {s : } (f : αβ) :
f <$> s = ### Pure # @[simp] theorem Finset.pure_def {α : Type u_1} : pure = singleton ### Applicative functor # instance Finset.applicative [(P : Prop) → ] : @[simp] theorem Finset.seq_def {α : Type u} {β : Type u} [(P : Prop) → ] (s : ) (t : Finset (αβ)) : (Seq.seq t fun x => s) = Finset.sup t fun f => @[simp] theorem Finset.seqLeft_def {α : Type u} {β : Type u} [(P : Prop) → ] (s : ) (t : ) : (SeqLeft.seqLeft s fun x => t) = if t = then else s @[simp] theorem Finset.seqRight_def {α : Type u} {β : Type u} [(P : Prop) → ] (s : ) (t : ) : (SeqRight.seqRight s fun x => t) = if s = then else t theorem Finset.image₂_def [(P : Prop) → ] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (f : αβγ) (s : ) (t : ) : = Seq.seq (f <$> s) fun x => t

Finset.image₂ in terms of monadic operations. Note that this can't be taken as the definition because of the lack of universe polymorphism.

instance Finset.lawfulApplicative [(P : Prop) → ] :
instance Finset.commApplicative [(P : Prop) → ] :

instance Finset.instMonadFinset [(P : Prop) → ] :
@[simp]
theorem Finset.bind_def [(P : Prop) → ] {α : Type u_1} {β : Type u_1} :
(fun x x_1 => x >>= x_1) = Finset.sup

### Traversable functor #

def Finset.traverse {α : Type u} {β : Type u} {F : Type u → Type u} [] [] [] (f : αF β) (s : ) :
F ()

Traverse function for Finset.

Instances For
@[simp]
theorem Finset.id_traverse {α : Type u} [] (s : ) :
@[simp]
theorem Finset.map_comp_coe {α : Type u} {β : Type u} (h : αβ) :
Multiset.toFinset = Multiset.toFinset
theorem Finset.map_traverse {α : Type u} {β : Type u} {γ : Type u} {G : Type u → Type u} [] [] (g : αG β) (h : βγ) (s : ) :