Documentation

Mathlib.Data.Set.Functor

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 = ⋃ 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 : Unit) => t) = Set.seq s 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

    Monadic coercion lemmas #

    theorem Set.mem_coe_of_mem {α : Type u} {β : Set α} {γ : Set β} {a : α} (ha : a β) (ha' : { val := a, property := ha } γ) :
    theorem Set.coe_subset {α : Type u} {β : Set α} {γ : Set β} :
    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 : αδ} :

    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.instCoeHeadSetElem {α : Type u} {s : Set α} :
    CoeHead (Set s) (Set α)

    Coercion using (Subtype.val '' ·)

    Equations
    • Set.instCoeHeadSetElem = { coe := fun (t : Set s) => Subtype.val '' t }
    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 defined above.

    theorem Set.mem_image_val_of_mem {α : Type u} {β : Set α} {γ : Set β} {a : α} (ha : a β) (ha' : { val := a, property := 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 '' γ) :
    { val := a, property := (_ : 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 '' γ) = Set.restrict β f '' γ

    Wrapper to enable the Set monad #

    def SetM (α : Type u) :

    This is Set but with a Monad instance.

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

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

      Equations
      Instances For