valid'_nil

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordnode.valid'_nil

English

If a nil node is bounded between o1 and o2, then it is Valid' o1 nil o2.

Русский

Если нулевой узел ограничен между o1 и o2, тогда он является Valid' o1 nil o2.

LaTeX

$$$\\forall o_1,o_2:\\; Bounded(nil, o_1, o_2) \\Rightarrow Ordnode.Valid' o_1 Ordnode.nil o_2.$$$

Lean4

theorem valid'_nil {o₁ o₂} (h : Bounded nil o₁ o₂) : Valid' o₁ (@nil α) o₂ :=
  ⟨h, ⟨⟩, ⟨⟩⟩

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

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

Разделы

Аффилиация

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