numLeaves_pos

Mathlib.Data.Tree.Basic

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

English

The number of leaves is positive for any tree.

Русский

Число листьев положительно для любого дерева.

LaTeX

$$$ 0 < \mathrm{numLeaves}(x). $$$

Lean4

theorem numLeaves_pos (x : Tree α) : 0 < x.numLeaves :=
  by
  rw [numLeaves_eq_numNodes_succ]
  exact x.numNodes.zero_lt_succ

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

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

Разделы

Аффилиация

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