mathlib documentation

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), decidable P] :

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

Equations
@[protected, instance]
@[simp]
theorem finset.fmap_def {α β : Type u} [Π (P : Prop), decidable P] {s : finset α} (f : α β) :

Pure #

@[protected, instance]
Equations

Applicative functor #

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

Monad #

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

Alternative functor #

Traversable functor #

def finset.traverse {α β : Type u} {F : Type u Type u} [applicative F] [is_comm_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 α) :
theorem finset.map_traverse {α β γ : Type u} {G : Type u Type u} [applicative G] [is_comm_applicative G] (g : α G β) (h : β γ) (s : finset α) :