Functoriality of Set

This file defines the functor structure of Set.

instance Set.monad : Monad Set

@[simp]

theorem Set.bind_def {α : Type u} {β : Type u} {s : Set α} {f : α → Set β} : s >>= f = ⋃ (i : α) (_ : i ∈ s), 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 => t) = Set.seq s t

@[simp]

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

theorem Set.image2_def {α : Type u_1} {β : Type u_1} {γ : Type u_1} (f : α → β → γ) (s : Set α) (t : Set β) : Set.image2 f s t = Seq.seq (f <$> s) fun x => 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.instLawfulMonadSetMonad : LawfulMonad Set

instance Set.instCommApplicativeSetToApplicativeMonad : CommApplicative Set

instance Set.instAlternativeSet : Alternative Set

Monadic coercion lemmas

theorem Set.mem_coe_of_mem {α : Type u} {β : Set α} {γ : Set ↑β} {a : α} (ha : a ∈ β) (ha' : { val := a, property := ha } ∈ γ) : a ∈ Lean.Internal.coeM γ

theorem Set.coe_subset {α : Type u} {β : Set α} {γ : Set ↑β} : Lean.Internal.coeM γ ⊆ β

theorem Set.mem_of_mem_coe {α : Type u} {β : Set α} {γ : Set ↑β} {a : α} (ha : a ∈ Lean.Internal.coeM γ) : { val := a, property := (_ : a ∈ β) } ∈ γ

theorem Set.eq_univ_of_coe_eq {α : Type u} {β : Set α} {γ : Set ↑β} (hγ : Lean.Internal.coeM γ = β) : γ = Set.univ

theorem Set.image_coe_eq_restrict_image {α : Type u} {β : Set α} {γ : Set ↑β} {δ : Type u_1} {f : α → δ} : f '' Lean.Internal.coeM γ = Set.restrict β f '' γ