stirlingFirst_succ_right — Mathlib

English

For n ≠ 0 and any k, StirlingFirst(n,k+1) = (n−1)·StirlingFirst(n−1,k+1) + StirlingFirst(n−1,k).

Русский

Пусть n ≠ 0. Тогда StirlingFirst(n,k+1) = (n−1)·StirlingFirst(n−1,k+1) + StirlingFirst(n−1,k).

LaTeX

$$$\forall n,k\ (n \ne 0) \Rightarrow \mathrm{stirlingFirst}(n,k+1) = (n-1)\,\mathrm{stirlingFirst}(n-1,k+1) + \mathrm{stirlingFirst}(n-1,k)$$$

Lean4

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

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