pow_const — Mathlib

English

If f is uniformly continuous, then for every natural n, the map x ↦ f(x)^n is uniformly continuous.

Русский

Если f равномерно непрерывна, то для любого натурального n отображение x ↦ f(x)^n равномерно непрерывно.

LaTeX

$$$\\mathrm{Uniformly\\;continuous}(f) \\rightarrow \\forall n:\\mathbb{N},\\ \\mathrm{Uniformly\\;continuous}(x \\mapsto f(x)^n)$$$

Lean4

@[to_additive UniformContinuous.const_nsmul]
theorem pow_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) : ∀ n : ℕ, UniformContinuous fun x => f x ^ n
  | 0 => by
    simp_rw [pow_zero]
    exact uniformContinuous_const
  | n + 1 => by
    simp_rw [pow_succ']
    exact hf.mul (hf.pow_const n)

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