pow_le_pow_of_le_one

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

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

Русский

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

LaTeX

$$$0 \\le a \\land a \\le 1 \\land m \\le n \\\\Rightarrow a^n \\le a^m.$$$

Lean4

theorem pow_le_pow_of_le_one [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ} (hmn : m ≤ n) : a ^ n ≤ a ^ m :=
  pow_right_anti₀ ha₀ ha₁ hmn

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

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

Разделы

Аффилиация

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