pow_lt_ascFactorial' — Mathlib

English

For all n,l,k ∈ ℕ, n^{\overline{l}} · (n+l)^{\overline{k}} = n^{\overline{l+k}}.

Русский

Для любых n,l,k ∈ ℕ: n^{\overline{l}} · (n+l)^{\overline{k}} = n^{\overline{l+k}}.

LaTeX

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

Lean4

theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2) :=
  by
  rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]
  exact
    Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos) (pow_succ_le_ascFactorial n.succ _)
      (Nat.pow_pos n.succ_pos)

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