nil

Mathlib.Data.Ordmap.Ordset

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

English

The empty Ordset is defined as nil, and has zero size.

Русский

Пустое Ordset определяется как nil и имеет нулевой размер.

LaTeX

$$$\\mathrm{Ordset}.nil : \\mathrm{Ordset}(\\alpha)$ и $|\\mathrm{Ordset}.nil| = 0$$$

Lean4

/-- O(1). The empty set. -/
nonrec def nil : Ordset α :=
  ⟨nil, ⟨⟩, ⟨⟩, ⟨⟩⟩

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

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

Разделы

Аффилиация

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