valid_singleton

Mathlib.Data.Ordmap.Ordset

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

English

The singleton tree with root x is a valid Ordnode.

Русский

Дерево-одиночка с корнем x является допустимым Ordnode.

LaTeX

$$$\\forall x:\\alpha, Ordnode.Valid( (singleton x) ).$$$

Lean4

theorem valid_singleton {x : α} : Valid (singleton x : Ordnode α) :=
  valid'_singleton ⟨⟩ ⟨⟩

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

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

Разделы

Аффилиация

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