size_eq — Mathlib

English

The size of a node equals the size of the left subtree plus the size of the right subtree plus one, when the node is Sized.

Русский

Размер узла равен размеру левого поддерева плюс размер правого поддерева плюс один, если узел имеет размер.

LaTeX

$$$\\forall s l x r\\ (H : Sized(\\mathrm{node} s l x r)),\\ \\mathrm{size}(\\mathrm{node} s l x r) = \\mathrm{size}(l) + \\mathrm{size}(r) + 1$$$

Lean4

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

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