binary_tree_num_leaves_le_pow_height
theoremverified
The number of leaves of any binary tree is at most 2 raised to its height.
Statement
theorem binary_tree_num_leaves_le_pow_height {α : Type*} (t : BinaryTree α) : t.numLeaves ≤ 2 ^ t.height
- Verified
- 06 Sep 2026
- Axioms
Quot.soundpropext- Used by 1
- comparison_sort_decision_tree_height_geIf a binary decision tree has at least n! leaves, then 2^(height) >= n!, establishing the comparison sorting lower bound.
Lean source view module on GitHub
/-- Every binary tree of height h has at most 2^h leaves. -/ theorem binary_tree_num_leaves_le_pow_height {α : Type*} (t : BinaryTree α) : t.numLeaves ≤ 2 ^ t.height := by induction t with | nil => simp | node _ a b ha hb => simp only [BinaryTree.numLeaves, BinaryTree.height] have h1 : 2 ^ a.height ≤ 2 ^ max a.height b.height := Nat.pow_le_pow_right (by omega) (le_max_left a.height b.height) have h2 : 2 ^ b.height ≤ 2 ^ max a.height b.height := Nat.pow_le_pow_right (by omega) (le_max_right a.height b.height) omega