zpow_le_zpow_left — Mathlib

English

If n ≤ 0, monotonicity in the exponent holds in a specific sense; in particular, for nonpositive n, a^n ≤ b^n when a ≤ b if the structure supports it.

Русский

Если n ≤ 0, то при сохранении порядка в степени выполняется нестрогое неравенство: при a ≤ b выполняется a^n ≤ b^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 (attr := gcongr) zsmul_le_zsmul_right]
theorem zpow_le_zpow_left (hn : 0 ≤ n) (h : a ≤ b) : a ^ n ≤ b ^ n :=
  zpow_left_mono α hn h

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