mathlib documentation

data.set.functor

Functoriality of set #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : α) :
theorem set.image2_def {α β γ : Type u_1} (f : α β γ) (s : set α) (t : set β) :
set.image2 f s t = f <$> s <*> 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.

@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations