pow_self_strictMonoOn — Mathlib

English

The function n ↦ n^n is strictly monotone on {n ∈ ℕ | n ≠ 0}.

Русский

Функция n ↦ n^n строго монотонна на {n ∈ ℕ | n ≠ 0}.

LaTeX

$$$\\mathrm{StrictMonoOn}(\\lambda n : \\mathbb{N} \\mapsto n^n)\\{n : \\mathbb{N} \\mid n \\neq 0\\}$$$

Lean4

theorem pow_self_strictMonoOn : StrictMonoOn (fun n : ℕ ↦ n ^ n) {n : ℕ | n ≠ 0} := fun _m hm _n hn hmn ↦
  (Nat.pow_lt_pow_left hmn hm).trans_le (Nat.pow_le_pow_right (Nat.pos_iff_ne_zero.2 hn) hmn.le)

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