stirlingFirst_eq_zero_of_lt — Mathlib

English

If n < k then StirlingFirst(n,k) = 0.

Русский

Если n < k, то StirlingFirst(n,k) = 0.

LaTeX

$$$n < k \Rightarrow \mathrm{stirlingFirst}(n,k) = 0$$$

Lean4

theorem stirlingFirst_eq_zero_of_lt : ∀ {n k : ℕ}, n < k → stirlingFirst n k = 0
  | _, 0, hk => absurd hk (Nat.not_lt_zero _)
  | 0, _ + 1, _ => by rw [stirlingFirst]
  | n + 1, k + 1, hk => by
    rw [stirlingFirst_succ_succ, stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt_succ hk),
      stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt hk), mul_zero]

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