size_eq — Mathlib

English

For a valid node, its size equals the sum of its children's sizes plus one.

Русский

Для допустимого узла размер равен сумме размеров левого и правого поддеревьев плюс единица.

LaTeX

$$$\\forall {s l x r}:\\ Ordnode(\\alpha)\\text{ } (H : Valid(@node α s l x r)) \\Rightarrow size(@node α s l x r) = size l + size r + 1.$$$

Lean4

theorem size_eq {s l x r} (H : Valid (@node α s l x r)) : size (@node α s l x r) = size l + size r + 1 :=
  H.2.1

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