stirlingFirst_succ_succ

Mathlib.Combinatorics.Enumerative.Stirling

URI: https://scilib.ai/kg/mathlib#Nat.stirlingFirst_succ_succ

English

StirlingFirst(n+1,k+1) = n·StirlingFirst(n,k+1) + StirlingFirst(n,k).

Русский

StirlingFirst(n+1,k+1) = n·StirlingFirst(n,k+1) + StirlingFirst(n,k).

LaTeX

$$$\mathrm{stirlingFirst}(n+1,k+1) = n\cdot \mathrm{stirlingFirst}(n,k+1) + \mathrm{stirlingFirst}(n,k)$$$

Lean4

theorem stirlingFirst_succ_succ (n k : ℕ) :
    stirlingFirst (n + 1) (k + 1) = n * stirlingFirst n (k + 1) + stirlingFirst n k := by rfl

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

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

Разделы

Аффилиация

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