node' — Mathlib

English

If left and right parts are valid, then a node built with node' is valid under the same bounds.

Русский

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

LaTeX

$$$\\forall l x r o_1 o_2:\\; (hl: Valid'(o_1, l, x)) \\wedge (hr: Valid'(x, r, o_2)) \\Rightarrow Valid'(o_1, (l.node' x r), o_2).$$$

Lean4

theorem node' {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂) (H : BalancedSz (size l) (size r)) :
    Valid' o₁ (@node' α l x r) o₂ :=
  hl.node hr H rfl

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