height — Mathlib

English

Height is the length of the longest root-to-leaf path.

Русский

Высота равна длине длиннейшего пути от корня до листа.

LaTeX

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

Lean4

/-- The height - length of the longest path from the root - of a binary tree -/
@[simp]
def height : Tree α → ℕ
  | nil => 0
  | node _ a b => max a.height b.height + 1

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