catalan_succ

Mathlib.Combinatorics.Enumerative.Catalan

URI: https://scilib.ai/kg/mathlib#catalan_succ

English

For any n, catalan(n+1) = ∑ i=0..n catalan(i) · catalan(n-i).

Русский

Для любого n выполняется catalan(n+1) = ∑_{i=0}^{n} catalan(i) · catalan(n-i).

LaTeX

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

Lean4

theorem catalan_succ (n : ℕ) : catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i) := by rw [catalan]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru