pow_lt_pow_right'

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

If 1 < a and n < m, then a^n < a^m.

Русский

Если 1 < a и n < m, то a^n < a^m.

LaTeX

$$$ 1 < a \land n < m \Rightarrow a^n < a^m $$$

Lean4

@[to_additive (attr := gcongr) nsmul_lt_nsmul_left]
theorem pow_lt_pow_right' (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
  pow_right_strictMono' ha h

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

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

Разделы

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

Аффилиация

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