mathlibdocumentation

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 #

@[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
@[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 uType 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 uType u} [applicative G] (g : α → G β) (h : β → γ) (s : finset α) :