size_node — Mathlib

English

In an ordered binary tree where each node stores its subtree size, the size stored at a node equals the size parameter sz of that node.

Русский

В упорядоченном двоичном дереве каждый узел хранит размер поддерева; размер, записанный в узле, равен значению sz этого узла.

LaTeX

$$$ \operatorname{size}(\operatorname{node}(sz, l, x, r)) = sz $$$

Lean4

@[simp]
theorem size_node (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : size (node sz l x r) = sz :=
  rfl

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