ascFactorial_lt_pow_add — Mathlib

English

(n - k) · (n - k + 1)^{\overline{k}} = (n - k)^{\overline{k+1}}.

Русский

(n - k) · (n - k + 1)^{\overline{k}} = (n - k)^{\overline{k+1}}.

LaTeX

$$$$\forall n,k \in \mathbb{N},\ (n-k) \cdot (n-k+1)^{\overline{k}} = (n-k)^{\overline{k+1}}$$$$

Lean4

theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ =>
    by
    rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
    exact
      Nat.mul_lt_mul_of_le_of_lt (le_refl _)
        (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _) (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero))
        (succ_pos _)

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