pow_lt_ascFactorial — Mathlib

English

For all n ∈ ℕ, ∀ k ∈ ℕ, n^k ≤ n^{\overline{k}}.

Русский

Для всех n ∈ ℕ, для каждого k ∈ ℕ верно: n^k ≤ n^{\overline{k}}.

LaTeX

$$$$\forall n \in \mathbb{N}, \forall k \in \mathbb{N},\ n^{k} \le n^{\overline{k}}$$$$

Lean4

theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => pow_lt_ascFactorial' n k

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