pow_const — Mathlib

English

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

Русский

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

LaTeX

$$$ (\text{Monotone } f) \Rightarrow (\forall n, \ Monotone (a \mapsto f(a)^n)) $$$

Lean4

@[to_additive Monotone.const_nsmul]
theorem pow_const {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n
  | 0 => by simpa using monotone_const
  | n + 1 => by
    simp_rw [pow_succ]
    exact (Monotone.pow_const hf _).mul' hf

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