zpow_left_mono — Mathlib

English

If n is a nonnegative integer, then the map x ↦ x^n is monotone (order-preserving).

Русский

Если n неотрицательно, то отображение x ↦ x^n сохраняет порядок.

LaTeX

$$$\forall n \in \mathbb{Z},\ 0 \le n \Rightarrow \forall a,b,\ a \le b \Rightarrow a^n \le b^n$$$

Lean4

@[to_additive zsmul_mono_right]
theorem zpow_left_mono (hn : 0 ≤ n) : Monotone ((· ^ n) : α → α) := fun a b hab => by rw [← one_le_div', ← div_zpow];
  exact one_le_zpow (one_le_div'.2 hab) hn

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