pow_le_pow_right_of_le_one'

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive nsmul_le_nsmul_left_of_nonpos]
theorem pow_le_pow_right_of_le_one' {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
  pow_le_pow_right' (M := Mᵒᵈ) ha h

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

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

Разделы

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

Аффилиация

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