# mathlib3documentation

data.finset.functor

# Functoriality of finset#

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

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 #

@[protected, instance]
def finset.functor [Π (P : Prop), ] :

Because finset.image requires a decidable_eq instance for the target type, we can only construct functor finset when working classically.

Equations
@[protected, instance]
def finset.is_lawful_functor [Π (P : Prop), ] :
@[simp]
theorem finset.fmap_def {α β : Type u} [Π (P : Prop), ] {s : finset α} (f : α β) :
f <$> s = s ### Pure # @[protected, instance] Equations @[simp] theorem finset.pure_def {α : Type u_1} : ### Applicative functor # @[protected, instance] def finset.applicative [Π (P : Prop), ] : Equations @[simp] theorem finset.seq_def {α β : Type u} [Π (P : Prop), ] (s : finset α) (t : finset β)) : t <*> s = t.sup (λ (f : α β), s) @[simp] theorem finset.seq_left_def {α β : Type u} [Π (P : Prop), ] (s : finset α) (t : finset β) : s <* t = ite (t = ) s @[simp] theorem finset.seq_right_def {α β : Type u} [Π (P : Prop), ] (s : finset α) (t : finset β) : s *> t = ite (s = ) t theorem finset.image₂_def [Π (P : Prop), ] {α β γ : Type u_1} (f : α β γ) (s : finset α) (t : finset β) : t = f <$> s <*> 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.

@[protected, instance]
def finset.is_lawful_applicative [Π (P : Prop), ] :
@[protected, instance]
def finset.is_comm_applicative [Π (P : Prop), ] :

@[protected, instance]
def finset.monad [Π (P : Prop), ] :
Equations
@[simp]
theorem finset.bind_def [Π (P : Prop), ] {α β : Type u_1} :
@[protected, instance]
def finset.is_lawful_monad [Π (P : Prop), ] :

### Alternative functor #

@[protected, instance]
def finset.alternative [Π (P : Prop), ] :
Equations

### Traversable functor #

def finset.traverse {α β : Type u} {F : Type u Type u} [applicative F] [decidable_eq β] (f : α F β) (s : finset α) :
F (finset β)

Traverse function for finset.

Equations
@[simp]
theorem finset.id_traverse {α : Type u} [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.map_comp_coe {α β : Type u} (h : α β) :
theorem finset.map_traverse {α β γ : Type u} {G : Type u Type u} [applicative G] (g : α G β) (h : β γ) (s : finset α) :