pow_le_pow_right'

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

If a ≥ 1 and n ≤ m, then a^n ≤ a^m.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := gcongr) nsmul_le_nsmul_left]
theorem pow_le_pow_right' {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
  pow_right_monotone ha h

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

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

Разделы

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

Аффилиация

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