pow_self_mono

Mathlib.Order.Monotone.Basic

URI: https://scilib.ai/kg/mathlib#Nat.pow_self_mono

← MathLib Explorer

English

The function n ↦ n^n is monotone on ℕ with its natural preorder.

Русский

Функция n ↦ n^n монотонна на ℕ по естественному порядку.

LaTeX

$$$\\mathrm{Monotone}(\\lambda n : \\mathbb{N}. n^n)$$$

Lean4

theorem pow_self_mono : Monotone fun n : ℕ ↦ n ^ n :=
  by
  refine monotone_nat_of_le_succ fun n ↦ ?_
  rw [Nat.pow_succ]
  exact (Nat.pow_le_pow_left n.le_succ _).trans (Nat.le_mul_of_pos_right _ n.succ_pos)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru