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

@[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.

Equations

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

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

Coercion from a set to the corresponding subtype.

Equations

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

@[simp]

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