uniformBell_succ_left — Mathlib

English

The recurrence is uniformBell(m+1,n) = C(mn+n−1, n−1) · uniformBell(m,n).

Русский

Рекуррентность слева: uniformBell(m+1,n) = C(mn+n−1, n−1) · uniformBell(m,n).

LaTeX

$$$ uniformBell(m+1,n) = {mn + n - 1 \\choose n - 1} \\cdot uniformBell(m,n) $$$

Lean4

theorem uniformBell_succ_left (m n : ℕ) : uniformBell (m + 1) n = choose (m * n + n - 1) (n - 1) * uniformBell m n := by
  simp only [uniformBell_eq, Finset.prod_range_succ, mul_comm]

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