left — Mathlib

English

If a node with left subtree is valid, then the left subtree with its root is valid under the same left bound.

Русский

Если узел с левым поддеревом допустим, то левое поддерево с корнем допустимо при той же левой границе.

LaTeX

$$$\\forall s,l,x,r,o_1,o_2:\\; (\\text{Ordnode.Valid}'(o_1,(\\mathrm{node}\\, s\\, l\\, x\\, r), o_2)) \\Rightarrow (\\text{Ordnode.Valid}'(o_1, l, x)).$$$

Lean4

theorem left {s l x r o₁ o₂} (H : Valid' o₁ (@Ordnode.node α s l x r) o₂) : Valid' o₁ l x :=
  ⟨H.1.1, H.2.2.1, H.3.2.1⟩

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