instSingletonSet — Mathlib

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⟩

Похожие утверждения