pow_right_strictMono₀ — Mathlib

English

If a > 1, then exponentiation by a is strictly increasing on natural numbers: m < n implies a^m < a^n.

Русский

Если a > 1, то возведение в степень на натуральных числах строго возрастает: m < n ⇒ a^m < a^n.

LaTeX

$$$1 < a \Rightarrow \forall m,n \in \mathbb{N}, \ m < n \Rightarrow a^m < a^n$$$

Lean4

/-- See also `pow_right_strictMono'`. -/
theorem pow_right_strictMono₀ (h : 1 < a) : StrictMono (a ^ ·) :=
  strictMono_nat_of_lt_succ fun n => by
    simpa only [one_mul, pow_succ] using lt_mul_right (pow_pos (zero_le_one.trans_lt h) _) h

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