# 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}`;

source
@[reducible]
def Set.Elem {α : Type u} (s : Set α) :
Type u

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.lean`.

Equations

- ↑s = { x : α // x ∈ s }

Instances For

source
instance Set.instCoeSortType {α : Type u} :
CoeSort (Set α) (Type u)

Coercion from a set to the corresponding subtype.

Equations

- Set.instCoeSortType = { coe := Set.Elem }

source
@[simp]
theorem Set.elem_mem {σ : Type u_1} {α : Type u_2} [I : Membership σ α] {S : α} :
↑(Membership.mem S) = { x : σ // x ∈ S }