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) → Decidable P] :

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

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • =
@[simp]
theorem Finset.fmap_def {α : Type u} {β : Type u} [(P : Prop) → Decidable P] {s : Finset α} (f : αβ) :

Pure #

Equations
@[simp]
theorem Finset.pure_def {α : Type u_1} :
pure = singleton

Applicative functor #

Equations
  • Finset.applicative = let __src := Finset.functor; let __src_1 := Finset.pure; Applicative.mk
@[simp]
theorem Finset.seq_def {α : Type u} {β : Type u} [(P : Prop) → Decidable P] (s : Finset α) (t : Finset (αβ)) :
(Seq.seq t fun (x : Unit) => s) = Finset.sup t fun (f : αβ) => Finset.image f s
@[simp]
theorem Finset.seqLeft_def {α : Type u} {β : Type u} [(P : Prop) → Decidable P] (s : Finset α) (t : Finset β) :
(SeqLeft.seqLeft s fun (x : Unit) => t) = if t = then else s
@[simp]
theorem Finset.seqRight_def {α : Type u} {β : Type u} [(P : Prop) → Decidable P] (s : Finset α) (t : Finset β) :
(SeqRight.seqRight s fun (x : Unit) => t) = if s = then else t
theorem Finset.image₂_def [(P : Prop) → Decidable P] {α : Type u} {β : Type u} {γ : Type u} (f : αβγ) (s : Finset α) (t : Finset β) :
Finset.image₂ f s t = Seq.seq (f <$> s) fun (x : Unit) => 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.

Equations
  • =
Equations
  • =

Monad #

Equations
  • Finset.instMonadFinset = let __src := Finset.applicative; Monad.mk
@[simp]
theorem Finset.bind_def [(P : Prop) → Decidable P] {α : Type u_1} {β : Type u_1} :
(fun (x : Finset β) (x_1 : βFinset α) => x >>= x_1) = Finset.sup

Alternative functor #

Equations

Traversable functor #

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

Traverse function for Finset.

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