valid_nil

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordnode.valid_nil

English

The empty tree is a valid Ordnode.

Русский

Пустое дерево является допустимым Ordnode.

LaTeX

$$$\\mathrm{Valid}(\\mathrm{nil}_{\\alpha}).$$$

Lean4

theorem valid_nil : Valid (@nil α) :=
  valid'_nil ⟨⟩

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

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

Разделы

Аффилиация

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