card_dyckWord_semilength_eq_catalan

English

The number of Dyck words of semilength n equals the Catalan number catalan n.

Русский

Число DyckWord семилength n равно Catalan(n).

LaTeX

$$Fintype.card { p : DyckWord // p.semilength = n } = \operatorname{catalan} n$$

Lean4

/-- There are `catalan n` Dyck words of semilength `n` (or length `2 * n`). -/
theorem card_dyckWord_semilength_eq_catalan (n : ℕ) : Fintype.card { p : DyckWord // p.semilength = n } = catalan n :=
  by
  rw [← Fintype.ofEquiv_card (equivTreesOfNumNodesEq n), ← treesOfNumNodesEq_card_eq_catalan]
  convert Fintype.card_coe _

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