zpow_left_strictMonoOn₀ — Mathlib

English

If n > 0 and the group has MulPosMono, then a ↦ a^n is strictly monotone on {a | a ≥ 0}.

Русский

Если n > 0 и множество содержит неотрицательные a, то функция a ↦ a^n строго монотонна на этом множестве.

LaTeX

$$$$0 < n \Rightarrow \text{StrictMonoOn}(a \mapsto a^{n}, \{a \mid 0 \le a\}).$$$$

Lean4

theorem zpow_left_strictMonoOn₀ [MulPosMono G₀] (hn : 0 < n) : StrictMonoOn (fun a : G₀ ↦ a ^ n) {a | 0 ≤ a} := by
  lift n to ℕ using hn.le; simpa using pow_left_strictMonoOn₀ (by cutsat)

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