Functoriality of Set

This file defines the functor structure of Set.

@[implicit_reducible]

instance Set.instAlternative : Alternative Set

@[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.seqLeft_def {α β : Type u} (s : Set α) (t : Set β) : s <* t = {a : α | a ∈ s ∧ t.Nonempty}

@[simp]

theorem Set.seqRight_def {α β : Type u} (s : Set α) (t : Set β) : s *> t = {a : β | s.Nonempty ∧ a ∈ t}

@[simp]

theorem Set.pure_def {α : Type u} (a : α) : pure a = {a}

@[simp]

theorem Set.failure_def {α : Type u} : failure = ∅

@[simp]

theorem Set.orElse_def {α : Type u} (s t : Set α) : (s <|> t) = s ∪ t

theorem Set.image2_def {α β γ : Type u} (f : α → β → γ) (s : Set α) (t : 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.instLawfulAlternative : LawfulAlternative Set

instance Set.instCommApplicative : CommApplicative Set

@[implicit_reducible]

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

Moreover, 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.

@[simp]

theorem Set.bind_def {α β : Type u} {s : Set α} {f : α → Set β} : s >>= f = ⋃ i ∈ s, f i

instance Set.instLawfulMonad : LawfulMonad Set

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) = β) : γ = 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 '' γ = β) : γ = 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.

@[implicit_reducible]

instance instAlternativeMonadSetM : AlternativeMonad SetM

instance instLawfulMonadSetM : LawfulMonad SetM

instance instLawfulAlternativeSetM : LawfulAlternative SetM

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

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