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]
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
.
Instances For
Coercion from a set to the corresponding subtype.
Equations
- Set.instCoeSortType = { coe := Set.Elem }
@[simp]