English
The cardinality of Trees(n) equals the Catalan number catalan(n).
Русский
Мощность множества Trees(n) равна каталанову числу catalan(n).
LaTeX
$$$\\#\\big( \\mathrm{Trees}(n) \\big) = \\mathrm{catalan}(n)$$$
Lean4
theorem treesOfNumNodesEq_card_eq_catalan (n : ℕ) : #(treesOfNumNodesEq n) = catalan n := by
induction n using Nat.case_strong_induction_on with
| hz => simp
| hi n ih =>
rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']
· apply sum_congr rfl
rintro ⟨i, j⟩ H
rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]
· simp_rw [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left]
aesop