zpow_left_strictMono — Mathlib

English

For any positive integer n, the map x |→ x^n is strictly increasing on the ordered structure.

Русский

Для любого положительного целого n отображение x ↦ x^n строго возрастает на упорядоченной структуре.

LaTeX

$$$\forall n \in \mathbb{Z},\ 0 < n \Rightarrow \forall x,y,\ x

Lean4

@[to_additive zsmul_strictMono_right]
theorem zpow_left_strictMono (hn : 0 < n) : StrictMono ((· ^ n) : α → α) := fun a b hab => by
  rw [← one_lt_div', ← div_zpow]; exact one_lt_zpow (one_lt_div'.2 hab) hn

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