Documentation

Mathlib.Data.Set.Functor

Functoriality of Set #

This file defines the functor structure of Set.

instance Set.monad :
Equations
@[simp]
theorem Set.bind_def {α : Type u} {β : Type u} {s : Set α} {f : αSet β} :
s >>= f = Set.unionᵢ fun i => Set.unionᵢ fun h => f i
@[simp]
theorem Set.fmap_eq_image {α : Type u} {β : Type u} {s : Set α} (f : αβ) :
f <$> s = f '' s
@[simp]
theorem Set.seq_eq_set_seq {α : Type u} {β : Type u} (s : Set (αβ)) (t : Set α) :
(Seq.seq s fun x => t) = Set.seq s t
@[simp]
theorem Set.pure_def {α : Type u} (a : α) :
pure a = {a}
theorem Set.image2_def {α : Type u_1} {β : Type u_1} {γ : Type u_1} (f : αβγ) (s : Set α) (t : Set β) :
Set.image2 f s t = Seq.seq (f <$> s) fun x => t

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

Equations