pow_left_monotoneOn

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#pow_left_monotoneOn

← MathLib Explorer

English

Let a ≥ 1 and hm n ≤ m, then a^n ≤ a^m.

Русский

Пусть a ≥ 1 и n ≤ m, тогда a^n ≤ a^m.

LaTeX

$$$ [(1 \\le a) \\land (n \\le m)] \\Rightarrow a^n \\le a^m $$$

Lean4

theorem pow_left_monotoneOn [PosMulMono M₀] [MulPosMono M₀] : MonotoneOn (fun a : M₀ ↦ a ^ n) {x | 0 ≤ x} :=
  fun _a ha _b _ hab ↦ pow_le_pow_left₀ ha hab _

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

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

Разделы

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

Аффилиация

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