zpow₀ — Mathlib

English

If f tends to a under l, then f(x)^m tends to a^m under l, for any m ∈ ℤ provided a ≠ 0 or m ≥ 0.

Русский

Если f(x) → a по фильтру l, то f(x)^m → a^m по l, для любого m ∈ ℤ при условии a ≠ 0 или m ≥ 0.

LaTeX

$$$\\text{Tendsto } f \\ l (\\mathcal{N}(a)) \\Rightarrow \\forall m:\\mathbb{Z},\\ (a \\neq 0 \\lor 0 \\le m) \\Rightarrow \\text{Tendsto}(x \\mapsto f(x)^{m})\\ l (\\mathcal{N}(a^{m}))$$$

Lean4

theorem zpow₀ {f : α → G₀} {l : Filter α} {a : G₀} (hf : Tendsto f l (𝓝 a)) (m : ℤ) (h : a ≠ 0 ∨ 0 ≤ m) :
    Tendsto (fun x => f x ^ m) l (𝓝 (a ^ m)) :=
  (continuousAt_zpow₀ _ m h).tendsto.comp hf

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