stirlingFirst_succ_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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