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 = 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

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

    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
      • s.run = s
      Instances For