realSize — Mathlib

English

The actual size of a node is the sum of the sizes of its left and right subtrees plus one for the node itself; this ignores any cached size.

Русский

Реальный размер узла равен сумме размеров левого и правого поддеревьев плюс один за сам узел, игнорируя кэшированный размер.

LaTeX

$$$\\mathrm{realSize}({\\mathrm{nil}}) = 0,\\qquad \\mathrm{realSize}(\\mathrm{node}\\ s\\ l\\ x\\ r) = \\mathrm{realSize}(l) + \\mathrm{realSize}(r) + 1$$$

Lean4

/-- O(n). Computes the actual number of elements in the set, ignoring the cached `size` field. -/
def realSize : Ordnode α → ℕ
  | nil => 0
  | node _ l _ r => realSize l + realSize r + 1

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