pow_le_pow_iff_right' — Mathlib

English

If a > 1 in M, then the map n ↦ a^n is monotone in n, hence a^m ≤ a^n if and only if m ≤ n.

Русский

Если a > 1 в M, тогда отображение n ↦ a^n монотонно по n, следовательно a^m ≤ a^n эквивалентно m ≤ n.

LaTeX

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

Lean4

@[to_additive nsmul_le_nsmul_iff_left]
theorem pow_le_pow_iff_right' (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
  (pow_right_strictMono' ha).le_iff_le

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