pow — Mathlib

English

For ENNReal, the map a ↦ a^n is continuous for each fixed natural n.

Русский

Для ENNReal отображение a ↦ a^n непрерывно для каждого фиксированного натурального n.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\text{Continuous } (\\\\lambda a, a^n) \\\\ on \\\\ ENNReal.$$$

Lean4

protected theorem pow {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} {n : ℕ} (hm : Tendsto m f (𝓝 a)) :
    Tendsto (fun x => m x ^ n) f (𝓝 (a ^ n)) :=
  ((ENNReal.continuous_pow n).tendsto a).comp hm

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