mathlib documentation

data.set.functor

Functoriality of set #

This file defines the functor structure of set.

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