singleton

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordset.singleton

English

There is a canonical singleton Ordset containing a single element a.

Русский

Существует каноническое одиночное Ordset, содержащее единственный элемент a.

LaTeX

$$$\\mathrm{Ordset}.singleton(a) \\in \\mathrm{Ordset}(\\alpha)$$$

Lean4

/-- O(1). Construct a singleton set containing value `a`. -/
protected def singleton (a : α) : Ordset α :=
  ⟨singleton a, valid_singleton⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru