mathlib documentation

data.set.functor

Functoriality of set #

This file defines the functor structure of set.

source
@[protected, instance]
def set.monad  :
monad set
Equations
source
@[simp]
theorem set.bind_def {α β : Type u} {s : set α} {f : α → set β} :
s >>= f = ⋃ (i : α) (H : i ∈ s), f i
source
@[simp]
theorem set.fmap_eq_image {α β : Type u} {s : set α} (f : α → β) :
f <$> s = f '' s
source
@[simp]
theorem set.seq_eq_set_seq {α β : Type u} (s : set (α → β)) (t : set α) :
s <*> t = s.seq t
source
@[simp]
theorem set.pure_def {α : Type u} (a : α) :
pure a = {a}
source
@[protected, instance]
def set.is_lawful_monad  :
is_lawful_monad set
source
@[protected, instance]
def set.is_comm_applicative  :
is_comm_applicative set
source
@[protected, instance]
def set.alternative  :
alternative set
Equations