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.

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 }

Documentation

Mathlib.Data.Set.CoeSort

Coercing sets to types. #

Main definitions #