pow_lt_pow_right₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If a > 1, then for any natural numbers m < n, a^m < a^n.

Русский

Если a > 1, то для любых натуральных чисел m < n выполняется a^m < a^n.

LaTeX

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

Lean4

@[gcongr]
theorem pow_lt_pow_right₀ (h : 1 < a) (hmn : m < n) : a ^ m < a ^ n :=
  pow_right_strictMono₀ h hmn

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

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

Разделы

Аффилиация

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