pow_left_strictMonoOn₀ — Mathlib

English

For every nonzero n, the map x ↦ x^n is strictly monotone on the set {x | x ≥ 0}.

Русский

Для каждого ненулевого n отображение x ↦ x^n является строго монотонным на множестве {x | x ≥ 0}.

LaTeX

$$$\forall n \neq 0, \ \forall x,y \ge 0, \ x < y \Rightarrow x^n < y^n$$$

Lean4

/-- See also `pow_left_strictMono₀` and `Nat.pow_left_strictMono`. -/
theorem pow_left_strictMonoOn₀ [MulPosMono M₀] (hn : n ≠ 0) : StrictMonoOn (· ^ n : M₀ → M₀) {a | 0 ≤ a} :=
  fun _a ha _b _ hab ↦ pow_lt_pow_left₀ hab ha hn

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