stirlingSecond_eq_zero_of_lt — Mathlib

English

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

Русский

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

LaTeX

$$$ n < k \Rightarrow {n \brace k} = 0 $$$

Lean4

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

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