mathlib3 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.

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 : α) :
has_pure.pure a = {a}
source
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.

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