valid'_singleton — Mathlib

English

There exists a valid singleton Ordnode for any bound pair if both bounds bound the singleton element.

Русский

Существует допустимое одиночное дерево для любого пар границ, если обе границы ограничивают одиночный элемент.

LaTeX

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

Lean4

theorem valid'_singleton {x : α} {o₁ o₂} (h₁ : Bounded nil o₁ x) (h₂ : Bounded nil x o₂) :
    Valid' o₁ (singleton x : Ordnode α) o₂ :=
  (valid'_nil h₁).node (valid'_nil h₂) (Or.inl zero_le_one) rfl

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