pow_right_strictMono'

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

URI: https://scilib.ai/kg/mathlib#pow_right_strictMono'

← MathLib Explorer

English

If 1 < a, then the map n ↦ a^n is strictly monotone in n.

Русский

Если 1 < a, то отображение n ↦ a^n строго монотонно по n.

LaTeX

$$$ 1 < a \Rightarrow (n < m \Rightarrow a^n < a^m) $$$

Lean4

@[to_additive nsmul_left_strictMono]
theorem pow_right_strictMono' (ha : 1 < a) : StrictMono ((a ^ ·) : ℕ → M) :=
  strictMono_nat_of_lt_succ fun n ↦ by rw [pow_succ]; exact lt_mul_of_one_lt_right' (a ^ n) ha

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

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

Разделы

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

Аффилиация

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