descFactorial_lt_pow — Mathlib

English

If 2 ≤ k ≤ n, then (n+1−k)^k < n.descFactorial k.

Русский

Если 2 ≤ k ≤ n, то (n+1−k)^k < n↓k.

LaTeX

$$(2 ≤ k) ∧ (k ≤ n) ⇒ (n + 1 - k)^{k} < n.descFactorial k$$

Lean4

theorem descFactorial_lt_pow {n : ℕ} (hn : n ≠ 0) : ∀ {k : ℕ}, 2 ≤ k → n.descFactorial k < n ^ k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => by
    rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]
    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (by omega) (Nat.pow_pos <| by omega)

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