Mathlib.Data.Set.CoeSort

Module docstring

{"# Coercing sets to types.

This file defines Set.Elem s as the type of all elements of the set s. More advanced theorems about these definitions are located in other files in Mathlib/Data/Set.

Main definitions

Set.Elem: coercion of a set to a type; it is reducibly equal to {x // x ∈ s}; "}

Set.Elem definition

(s : Set α) : Type u

Full source

/-- Given the set `s`, `Elem s` is the `Type` of element of `s`.

It is currently an abbreviation so that instance coming from `Subtype` are available.
If you're interested in making it a `def`, as it probably should be,
you'll then need to create additional instances (and possibly prove lemmas about them).
See e.g. `Mathlib.Data.Set.Order`.
-/
@[coe, reducible] def Elem (s : Set α) : Type u := {x // x ∈ s}

Type of elements of a set

Informal description

Given a set $s$ over a type $\alpha$, $\mathrm{Elem}\, s$ is the type of elements of $s$, which is equivalent to the subtype $\{x \mid x \in s\}$.

Set.instCoeSortType instance

: CoeSort (Set α) (Type u)

Full source

/-- Coercion from a set to the corresponding subtype. -/
instance : CoeSort (Set α) (Type u) := ⟨Elem⟩

Coercion from Sets to Types

Informal description

For any type $\alpha$ and set $s$ over $\alpha$, there is a canonical way to view $s$ as a type, where the elements of this type are exactly the elements of $s$. This type is equivalent to the subtype $\{x \mid x \in s\}$.

Set.elem_mem theorem

{σ α} [I : Membership σ α] {S} : @Set.Elem σ (@Membership.mem σ α I S) = { x // x ∈ S }

Full source

@[simp] theorem elem_mem {σ α} [I : Membership σ α] {S} :
    @Set.Elem σ (@Membership.mem σ α I S) = { x // x ∈ S } := rfl

Equivalence of `Set.Elem` and Subtype Construction

Informal description

For any type $\alpha$ with a membership relation `[Membership σ α]` and any set $S$ over $\alpha$, the type `Set.Elem S` is definitionally equal to the subtype $\{x \mid x \in S\}$.