uniformContinuous_pow_const — Mathlib

English

For any natural n, the map x ↦ x^n on α is uniformly continuous.

Русский

Для любого натурального n отображение x^n на α является равномерно непрерывным.

LaTeX

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

Lean4

@[to_additive uniformContinuous_const_nsmul]
theorem uniformContinuous_pow_const (n : ℕ) : UniformContinuous fun x : α => x ^ n :=
  uniformContinuous_id.pow_const n

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