numLeaves_eq_numNodes_succ

Mathlib.Data.Tree.Basic

URI: https://scilib.ai/kg/mathlib#Tree.numLeaves_eq_numNodes_succ

← MathLib Explorer

English

The number of leaves equals the number of internal nodes plus one.

Русский

Число листьев равно числу внутренних узлов плюс единица.

LaTeX

$$$ \mathrm{numLeaves}(x) = \mathrm{numNodes}(x) + 1. $$$

Lean4

theorem numLeaves_eq_numNodes_succ (x : Tree α) : x.numLeaves = x.numNodes + 1 := by
  induction x <;> simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru