# Functoriality of Set#

This file defines the functor structure of Set.

The Set functor is a monad.

This is not a global instance because it does not have computational content, so it does not make much sense using do notation in general. Plus, this would cause monad-related coercions and monad lifting logic to become activated. Either use attribute [local instance] Set.monad to make it be a local instance or use SetM.run do ... when do notation is wanted.

Equations
Instances For
@[simp]
theorem Set.bind_def {α : Type u} {β : Type u} {s : Set α} {f : αSet β} :
s >>= f = is, 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 : Unit) => t) = s.seq t @[simp] theorem Set.pure_def {α : Type u} (a : α) : pure a = {a} theorem Set.image2_def {α : Type u} {β : Type u} {γ : Type u} (f : αβγ) (s : Set α) (t : Set β) : Set.image2 f s t = Seq.seq (f <$> s) fun (x : Unit) => 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
Equations
Equations

theorem Set.mem_coe_of_mem {α : Type u} {β : Set α} {γ : Set β} {a : α} (ha : a β) (ha' : a, ha γ) :
a do let aγ pure a
theorem Set.coe_subset {α : Type u} {β : Set α} {γ : Set β} :
(do let aγ pure a) β
theorem Set.mem_of_mem_coe {α : Type u} {β : Set α} {γ : Set β} {a : α} (ha : a do let aγ pure a) :
a, γ
theorem Set.eq_univ_of_coe_eq {α : Type u} {β : Set α} {γ : Set β} (hγ : (do let aγ pure a) = β) :
γ = Set.univ
theorem Set.image_coe_eq_restrict_image {α : Type u} {β : Set α} {γ : Set β} {δ : Type u_1} {f : αδ} :
(f '' do let aγ pure a) = β.restrict f '' γ

### Coercion applying functoriality for Subtype.val#

The Monad instance gives a coercion using the internal function Lean.Internal.coeM. In practice this is only used for applying the Set functor to Subtype.val. We define this coercion here.

instance Set.instCoeHeadElem {α : Type u} {s : Set α} :

Coercion using (Subtype.val '' ·)

Equations
• Set.instCoeHeadElem = { coe := fun (t : Set s) => Subtype.val '' t }

If the Set.Notation namespace is open, sets of a subtype coerced to the ambient type are represented with ↑.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Set.coe_eq_image_val {α : Type u} {s : Set α} (t : Set s) :
= Subtype.val '' t

The coercion from Set.monad as an instance is equal to the coercion defined above.

theorem Set.mem_image_val_of_mem {α : Type u} {β : Set α} {γ : Set β} {a : α} (ha : a β) (ha' : a, ha γ) :
a Subtype.val '' γ
theorem Set.image_val_subset {α : Type u} {β : Set α} {γ : Set β} :
Subtype.val '' γ β
theorem Set.mem_of_mem_image_val {α : Type u} {β : Set α} {γ : Set β} {a : α} (ha : a Subtype.val '' γ) :
a, γ
theorem Set.eq_univ_of_image_val_eq {α : Type u} {β : Set α} {γ : Set β} (hγ : Subtype.val '' γ = β) :
γ = Set.univ
theorem Set.image_image_val_eq_restrict_image {α : Type u} {β : Set α} {γ : Set β} {δ : Type u_1} {f : αδ} :
f '' (Subtype.val '' γ) = β.restrict f '' γ

### Wrapper to enable the Set monad #

def SetM (α : Type u) :

This is Set but with a Monad instance.

Equations
Instances For
Evaluates the SetM monad, yielding a Set. Implementation note: this is the identity function.