stirlingFirst_succ_self_left — Mathlib

English

StirlingFirst(n+1,n) = (n+1 choose 2).

Русский

StirlingFirst(n+1,n) = \binom{n+1}{2}.

LaTeX

$$$\mathrm{stirlingFirst}(n+1,n) = \binom{n+1}{2}$$$

Lean4

theorem stirlingFirst_succ_self_left (n : ℕ) : stirlingFirst (n + 1) n = (n + 1).choose 2 := by
  induction n with
  | zero => simp only [zero_add, stirlingFirst_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1), Nat.choose_one_right]

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