catalan_succ' — Mathlib

English

catalan(n+1) = sum_{ij ∈ antidiagonal(n)} catalan(i) · catalan(j).

Русский

catalan(n+1) = сумма по парям i,j ∈ antidiagonal(n) catalan(i) · catalan(j).

LaTeX

$$$ catalan(n+1) = \\sum_{ij \\in \\mathrm{antidiagonal}(n)} catalan(i) \\cdot catalan(j) $$$

Lean4

theorem catalan_succ' (n : ℕ) : catalan (n + 1) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2 := by
  rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n, sum_range]

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