right — Mathlib

English

If a node is valid, then the right subtree is valid under the corresponding 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}'(x, r, o_2)).$$$

Lean4

theorem right {s l x r o₁ o₂} (H : Valid' o₁ (@Ordnode.node α s l x r) o₂) : Valid' x r o₂ :=
  ⟨H.1.2, H.2.2.2, H.3.2.2⟩

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