pow_right_monotone — Mathlib

English

If a ≥ 1, then the map n ↦ a^n is monotone on N; in particular, n ≤ m implies a^n ≤ a^m.

Русский

Если a ≥ 1, то отображение n ↦ a^n монотонно на натуральных числах: n ≤ m ⇒ a^n ≤ a^m.

LaTeX

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

Lean4

@[to_additive nsmul_left_monotone]
theorem pow_right_monotone (ha : 1 ≤ a) : Monotone fun n : ℕ ↦ a ^ n :=
  monotone_nat_of_le_succ fun n ↦ by rw [pow_succ]; exact le_mul_of_one_le_right' ha

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