catalan — Mathlib

English

The Catalan numbers are defined by catalan(0) = 1 and catalan(n+1) = sum_{i=0}^n catalan(i) · catalan(n-i).

Русский

Числа Каталана задаются рекуррентно: catalan(0) = 1 и catalan(n+1) = ∑_{i=0}^n catalan(i) · catalan(n-i).

LaTeX

$$$ catalan(0) = 1, \\quad catalan(n+1) = \\sum_{i=0}^{n} catalan(i) \\cdot catalan(n-i) $$$

Lean4

/-- The recursive definition of the sequence of Catalan numbers:
`catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i)` -/
def catalan : ℕ → ℕ
  | 0 => 1
  | n + 1 => ∑ i : Fin n.succ, catalan i * catalan (n - i)

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