English
There is a canonical map that sends every element a of α to the singleton subset {a} ⊆ α, i.e., a ↦ {a} : α → Set α.
Русский
Существует каноническое отображение, которое каждому элементу a типа α сопоставляет единичное множество {a} ⊆ α, то есть функцию a ↦ {a} из α в Set α.
LaTeX
$$$\exists f:\alpha \to Set\,\alpha,\ \forall a:\alpha,\ f(a)=\{a\}$$$
Lean4
instance instSingletonSet : Singleton α (Set α) :=
⟨Set.singleton⟩