pow_antitone_exp

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.pow_antitone_exp

English

Let a ∈ ℝ≥0 with a ≤ 1, and m,n ∈ ℕ with m ≤ n. Then a^n ≤ a^m.

Русский

Пусть a ∈ ℝ≥0 и a ≤ 1, и m,n ∈ ℕ с m ≤ n. Тогда a^n ≤ a^m.

LaTeX

$$$\forall a \in \mathbb{R}_{\ge 0},\ a \le 1\ \Rightarrow\ \forall m,n \in \mathbb{N},\ m \le n\ \Rightarrow\ a^n \le a^m$$$

Lean4

theorem pow_antitone_exp {a : ℝ≥0} (m n : ℕ) (mn : m ≤ n) (a1 : a ≤ 1) : a ^ n ≤ a ^ m :=
  pow_le_pow_of_le_one (zero_le a) a1 mn

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

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

Разделы

Аффилиация

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