continuous_zpow — Mathlib

English

For every integer n, the map x ↦ x^n is a continuous function on the extended nonnegative reals.

Русский

Для каждого целого n функция x ↦ x^n непрерывна на расширенных неотрицательных вещественных числах.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; \\text{Continuous}(x \\mapsto x^{n} : \\mathbb{R}_{\\ge 0}^{\\infty} \\to \\mathbb{R}_{\\ge 0}^{\\infty}).$$$

Lean4

@[fun_prop]
protected theorem continuous_zpow : ∀ n : ℤ, Continuous (· ^ n : ℝ≥0∞ → ℝ≥0∞)
  | (n : ℕ) => mod_cast ENNReal.continuous_pow n
  | .negSucc n => by simpa using (ENNReal.continuous_pow _).inv

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