Functoriality of Set

This file defines the functor structure of Set.

def Set.monad : Monad 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

• Set.monad = Monad.mk

@[simp]

theorem Set.bind_def {α β : Type u} {s : Set α} {f : α → Set β} : s >>= f = ⋃ 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}

theorem Set.image2_def {α β γ : Type u} (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.

instance Set.instLawfulMonad : LawfulMonad Set

instance Set.instCommApplicative : CommApplicative Set

instance Set.instAlternative : Alternative Set

Equations

• Set.instAlternative = Alternative.mk (fun {α : Type ?u.10} => ∅) fun {α : Type ?u.10} (s : Set α) (t : Unit → Set α) => s ∪ t ()

Monadic coercion lemmas

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, as was defined in Data.Set.Notation.

theorem Set.coe_eq_image_val {α : Type u} {s : Set α} (t : Set ↑s) : Lean.Internal.coeM t = Subtype.val '' t

The coercion from Set.monad as an instance is equal to the coercion in Data.Set.Notation.

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) : Type u

This is Set but with a Monad instance.

Equations

• SetM α = Set α

instance instMonadSetM : Monad SetM

Equations

• instMonadSetM = Set.monad

def SetM.run {α : Type u_1} (s : SetM α) : Set α

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

Equations

• s.run = s