treesOfNumNodesEq_card_eq_catalan

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

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