Mathlib.Data.Set.Functor

Set.monad definition

: Monad.{u} Set

Full source

/-- 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. -/
protected def monad : Monad.{u} Set where
  pure a := {a}
  bind s f := ⋃ i ∈ s, f i
  seq s t := Set.seq s (t ())
  map := Set.image

Monad structure on Set

Informal description

The `Set` type constructor forms a monad, where: - The `pure` operation sends an element $a$ to the singleton set $\{a\}$. - The `bind` operation for a set $s$ and a function $f$ is the union $\bigcup_{i \in s} f(i)$. - The `map` operation is given by the direct image of a function on sets. This is not declared as a global instance to avoid unintended activation of monadic operations and coercions. It can be locally instantiated when needed.

Set.bind_def theorem

: s >>= f = ⋃ i ∈ s, f i

Full source

@[simp]
theorem bind_def : s >>= f = ⋃ i ∈ s, f i :=
  rfl

Monadic Bind as Union for Sets

Informal description

For any set $s$ and any function $f$, the monadic bind operation $s \mathbin{>>=} f$ is equal to the union $\bigcup_{i \in s} f(i)$.

Set.fmap_eq_image theorem

(f : α → β) : f <$> s = f '' s

Full source

@[simp]
theorem fmap_eq_image (f : α → β) : f <$> s = f '' s :=
  rfl

Functorial Map Equals Direct Image for Sets

Informal description

For any function $f : \alpha \to \beta$ and any set $s \subseteq \alpha$, the image of $s$ under the functorial map operation $f <$> $s$ is equal to the direct image $f '' s$ (the set $\{f(x) \mid x \in s\}$).

Set.seq_eq_set_seq theorem

(s : Set (α → β)) (t : Set α) : s <*> t = s.seq t

Full source

@[simp]
theorem seq_eq_set_seq (s : Set (α → β)) (t : Set α) : s <*> t = s.seq t :=
  rfl

Monadic Sequencing Equals Set-Theoretic Sequencing for Sets

Informal description

For any set $s$ of functions from $\alpha$ to $\beta$ and any set $t$ of elements of $\alpha$, the monadic sequencing operation $s \mathbin{<*>} t$ is equal to the set-theoretic sequencing operation $s.\text{seq}\ t$, where both operations apply each function in $s$ to each element in $t$ and collect the results.

Set.pure_def theorem

(a : α) : (pure a : Set α) = { a }

Full source

@[simp]
theorem pure_def (a : α) : (pure a : Set α) = {a} :=
  rfl

Singleton Set via Monadic Pure Operation

Informal description

For any element $a$ of type $\alpha$, the monadic `pure` operation on sets returns the singleton set $\{a\}$, i.e., $\mathrm{pure}(a) = \{a\}$.

Set.image2_def theorem

{α β γ : Type u} (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = f <$> s <*> t

Full source

/-- `Set.image2` in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism. -/
theorem image2_def {α β γ : Type u} (f : α → β → γ) (s : Set α) (t : Set β) :
    image2 f s t = f <$> sf <$> s <*> t := by
  ext
  simp

Image of Binary Function via Monadic Operations

Informal description

For any function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of $f$ over $s$ and $t$ is equal to the monadic application of $f$ to $s$ and $t$, i.e., \[ \text{image2}(f, s, t) = f <\$> s <\*> t. \]

Set.instLawfulMonad instance

: LawfulMonad Set

Full source

instance : LawfulMonad Set := LawfulMonad.mk'
  (id_map := image_id)
  (pure_bind := biUnion_singleton)
  (bind_assoc := fun _ _ _ => by simp only [bind_def, biUnion_iUnion])
  (bind_pure_comp := fun _ _ => (image_eq_iUnion _ _).symm)
  (bind_map := fun _ _ => seq_def.symm)

The Lawful Monad Structure on Sets

Informal description

The `Set` type constructor forms a lawful monad, where: - The `pure` operation sends an element $a$ to the singleton set $\{a\}$. - The `bind` operation for a set $s$ and a function $f$ is the union $\bigcup_{i \in s} f(i)$. - The monad laws (left identity, right identity, and associativity) are satisfied. This instance ensures that the monadic operations on sets behave correctly with respect to the monad laws.

Set.instCommApplicative instance

: CommApplicative (Set : Type u → Type u)

Full source

instance : CommApplicative (Set : Type u → Type u) :=
  ⟨fun s t => prod_image_seq_comm s t⟩

Commutative Applicative Structure on Sets

Informal description

The `Set` type constructor forms a commutative applicative functor, where: - The `pure` operation sends an element $a$ to the singleton set $\{a\}$. - The sequential application operation for sets $s$ and $t$ satisfies the commutativity property $f <\$> s <\*> t = (\lambda a b \mapsto f b a) <\$> t <\*> s$ for any function $f$. This means that the order of application between two sets does not affect the resulting set of applications.

Set.instAlternative instance

: Alternative Set

Full source

instance : Alternative Set :=
  { Set.monad with
    orElse := fun s t => s ∪ (t ())
    failure := ∅ }

Alternative Functor Structure on Sets

Informal description

The `Set` type constructor forms an alternative functor structure, providing operations for choice and failure handling in addition to the standard functor operations. Specifically: - The `pure` operation sends an element $a$ to the singleton set $\{a\}$. - The `<|>` operation takes the union of two sets. - The `failure` operation returns the empty set. This structure extends the monad structure on `Set` with additional operations for handling alternatives.

Set.mem_coe_of_mem theorem

{a : α} (ha : a ∈ β) (ha' : ⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α)

Full source

theorem mem_coe_of_mem {a : α} (ha : a ∈ β) (ha' : ⟨a, ha⟩⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α) :=
  ⟨_, ⟨⟨_, rfl⟩, _, ⟨ha', rfl⟩, rfl⟩⟩

Membership Preservation under Subtype Coercion to Set

Informal description

Let $a$ be an element of type $\alpha$ such that $a \in \beta$ and $\langle a, ha \rangle \in \gamma$, where $\gamma$ is a set of subtype elements of $\beta$. Then $a$ belongs to the coercion of $\gamma$ to $\text{Set } \alpha$.

Set.coe_subset theorem

: (γ : Set α) ⊆ β

Full source

theorem coe_subset : (γ : Set α) ⊆ β := by
  intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩; convert ha

Subset Property of Coerced Sets

Informal description

For any subset $\gamma$ of a type $\alpha$ (viewed as a set), $\gamma$ is a subset of $\beta$, i.e., $\gamma \subseteq \beta$.

Set.mem_of_mem_coe theorem

{a : α} (ha : a ∈ (γ : Set α)) : ⟨a, coe_subset ha⟩ ∈ γ

Full source

theorem mem_of_mem_coe {a : α} (ha : a ∈ (γ : Set α)) : ⟨a, coe_subset ha⟩⟨a, coe_subset ha⟩ ∈ γ := by
  rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩; convert ha

Membership in Subtype via Coercion to Set

Informal description

For any element $a$ of type $\alpha$ such that $a$ belongs to the coercion of $\gamma$ to $\text{Set } \alpha$, the pair $\langle a, \text{coe\_subset } ha \rangle$ belongs to $\gamma$.

Set.image_coe_eq_restrict_image theorem

{δ : Type*} {f : α → δ} : f '' γ = β.restrict f '' γ

Full source

theorem image_coe_eq_restrict_image {δ : Type*} {f : α → δ} : f '' γ = β.restrict f '' γ :=
  ext fun _ =>
    ⟨fun ⟨_, h, ha⟩ => ⟨_, mem_of_mem_coe h, ha⟩, fun ⟨_, h, ha⟩ => ⟨_, mem_coe_of_mem _ h, ha⟩⟩

Image under Function Equals Image under Restricted Function

Informal description

For any function $f \colon \alpha \to \delta$, the image of the subset $\gamma$ under $f$ is equal to the image of $\gamma$ under the restriction of $f$ to $\beta$. That is, $f(\gamma) = f|_\beta(\gamma)$.

Set.coe_eq_image_val theorem

(t : Set s) : @Lean.Internal.coeM Set s α _ Set.monad t = (t : Set α)

Full source

/-- The coercion from `Set.monad` as an instance is equal to the coercion in `Data.Set.Notation`. -/
theorem coe_eq_image_val (t : Set s) :
    @Lean.Internal.coeM Set s α _ Set.monad t = (t : Set α) := by
  change ⋃ (x ∈ t), {x.1} = _
  ext
  simp

Monadic Coercion Equals Set Image under Inclusion

Informal description

For any subset $t$ of a set $s$, the coercion of $t$ via the `Set` monad is equal to the image of $t$ under the canonical inclusion map from $s$ to $\alpha$. In other words, the monadic coercion of $t$ coincides with the set-theoretic image of $t$ under the inclusion map.

Set.mem_image_val_of_mem theorem

(ha : a ∈ β) (ha' : ⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α)

Full source

theorem mem_image_val_of_mem (ha : a ∈ β) (ha' : ⟨a, ha⟩⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α) :=
  ⟨_, ha', rfl⟩

Membership in Coerced Image of Subset

Informal description

For any element $a$ in a set $\beta$ and any subset $\gamma$ of $\beta$, if the pair $\langle a, ha \rangle$ belongs to $\gamma$ (where $ha$ is a proof that $a \in \beta$), then $a$ belongs to the image of $\gamma$ under the canonical coercion to $\alpha$.

Set.image_val_subset theorem

: (γ : Set α) ⊆ β

Full source

theorem image_val_subset : (γ : Set α) ⊆ β := by
  rintro _ ⟨⟨_, ha⟩, _, rfl⟩; exact ha

Subset Property of Set-Valued Coercion

Informal description

For any subset $\gamma$ of a type $\alpha$ viewed as a set-valued coercion, $\gamma$ is a subset of $\beta$.

Set.mem_of_mem_image_val theorem

(ha : a ∈ (γ : Set α)) : ⟨a, image_val_subset ha⟩ ∈ γ

Full source

theorem mem_of_mem_image_val (ha : a ∈ (γ : Set α)) : ⟨a, image_val_subset ha⟩⟨a, image_val_subset ha⟩ ∈ γ := by
  rcases ha with ⟨_, ha, rfl⟩; exact ha

Membership in Subset via Coercion Image

Informal description

For any element $a$ in the image of $\gamma$ under the canonical coercion to $\alpha$, the pair $\langle a, h \rangle$ belongs to $\gamma$, where $h$ is a proof that $a$ is in $\beta$ obtained from the subset property of the coercion.

Set.image_image_val_eq_restrict_image theorem

{δ : Type*} {f : α → δ} : f '' γ = β.restrict f '' γ

Full source

theorem image_image_val_eq_restrict_image {δ : Type*} {f : α → δ} : f '' γ = β.restrict f '' γ := by
  ext; simp

Image Equals Restricted Image for Subset $\gamma$

Informal description

For any function $f \colon \alpha \to \delta$ and subset $\gamma \subseteq \alpha$, the image of $\gamma$ under $f$ equals the image of $\gamma$ under the restriction of $f$ to $\beta$, i.e., $$ f(\gamma) = (f|_\beta)(\gamma) $$ where $f|_\beta$ denotes the restriction of $f$ to $\beta$.

SetM definition

(α : Type u)

Full source

/-- This is `Set` but with a `Monad` instance. -/
def SetM (α : Type u) := Set α

Monadic set type

Informal description

The type `SetM α` is defined as the type of sets of elements of type `α`, equipped with a monad instance to enable functorial operations on sets.

instMonadSetM instance

: Monad SetM

Full source

instance : Monad SetM := Set.monad

Monad Structure on SetM

Informal description

The type constructor `SetM` forms a monad, where: - The `pure` operation sends an element $a$ to the singleton set $\{a\}$. - The `bind` operation for a set $s$ and a function $f$ is the union $\bigcup_{i \in s} f(i)$. - The `map` operation is given by the direct image of a function on sets. This monad structure enables functorial operations on sets, but is not declared as a global instance to avoid unintended activation of monadic operations and coercions.

SetM.run definition

{α : Type*} (s : SetM α) : Set α

Full source

/-- Evaluates the `SetM` monad, yielding a `Set`.
Implementation note: this is the identity function. -/
protected def SetM.run {α : Type*} (s : SetM α) : Set α := s

Evaluation of monadic set

Informal description

The function evaluates a monadic set `s : SetM α` to yield a set of elements of type `α`. This is implemented as the identity function, simply returning the input set `s`.