pow_const — Mathlib

English

If f is strictly monotone, then for every n ≠ 0, the map a ↦ f(a)^n is strictly monotone.

Русский

Если f строго монотонна, то для каждого n ≠ 0 отображение a ↦ f(a)^n является строго монотонным.

LaTeX

$$$ (\text{StrictMono } f) \Rightarrow (\forall n \neq 0, \ StrictMono (a \mapsto f(a)^n)) $$$

Lean4

@[to_additive StrictMono.const_nsmul]
theorem pow_const (hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → StrictMono (f · ^ n)
  | 0, hn => (hn rfl).elim
  | 1, _ => by simpa
  | Nat.succ <| Nat.succ n, _ => by simpa only [pow_succ] using (hf.pow_const n.succ_ne_zero).mul' hf

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