English
The elements of a set s form the corresponding subtype, i.e., the type of pairs (x, p) where x ∈ α and p is a proof that x ∈ s.
Русский
Элементы множества s образуют соответствующий подтекст, то есть тип пар (x, p), где x ∈ α и p — доказательство того, что x ∈ s.
LaTeX
$$$\mathrm{Elem}(s) = \{ (x, p) \mid x \in \alpha \land p : x \in s \}$$$
Lean4
/-- 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`.
-/
@[coe, reducible]
def Elem (s : Set α) : Type u :=
{ x // x ∈ s }
