stirlingSecond_succ_left — Mathlib

English

For natural n,k with k ≠ 0, the recurrence holds: {n+1 \brace k} = k {n \brace k} + {n \brace k-1}.

Русский

Для натуральных n,k с k ≠ 0 выполняется рекуррентность: {n+1 \brace k} = k {n \brace k} + {n \brace k-1}.

LaTeX

$$$ \forall n,k \in \mathbb{N},\ k \neq 0 \Rightarrow {n+1 \brace k} = k {n \brace k} + {n \brace k-1}$$$

Lean4

theorem stirlingSecond_succ_left (n k : ℕ) (hk : k ≠ 0) :
    stirlingSecond (n + 1) k = k * stirlingSecond n k + stirlingSecond n (k - 1) :=
  by
  obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hk)
  rfl

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