numLeaves — Mathlib

English

Definition of the number of leaves: a leaf counts as one; internal nodes sum leaves of their subtrees.

Русский

Определение числа листьев: лист считается за 1; узлы внутри дерева суммируют листья левых и правых поддеревьев.

LaTeX

$$$ \mathrm{numLeaves}(\mathrm{nil}) = 1, \quad \mathrm{numLeaves}(\mathrm{node}(v,a,b)) = \mathrm{numLeaves}(a) + \mathrm{numLeaves}(b). $$$

Lean4

/-- The number of leaves of a binary tree -/
@[simp]
def numLeaves : Tree α → ℕ
  | nil => 1
  | node _ a b => a.numLeaves + b.numLeaves

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