height_le_numNodes — Mathlib

English

The height of a tree is at most the number of internal nodes.

Русский

Высота дерева не превосходит число внутренних узлов.

LaTeX

$$$ \mathrm{height}(x) \le \mathrm{numNodes}(x). $$$

Lean4

theorem height_le_numNodes : ∀ x : Tree α, x.height ≤ x.numNodes
  | nil => Nat.le_refl _
  | node _ a b =>
    Nat.succ_le_succ <|
      Nat.max_le.2
        ⟨Nat.le_trans a.height_le_numNodes <| a.numNodes.le_add_right _,
          Nat.le_trans b.height_le_numNodes <| b.numNodes.le_add_left _⟩

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