zpow — Mathlib

English

If f converges to x under l, then the sequence f(z) converges to x^z under l for any integer z.

Русский

Если f сходится к x по фильтру l, то f^z сходится к x^z по l для любого целого z.

LaTeX

$$$(\text{Tendsto } f\ l\ (\mathcal{N} x)) \Rightarrow \text{Tendsto}(\lambda y. f(y)^{z})\ l\ (\mathcal{N}(x^{z})).$$$

Lean4

@[to_additive]
theorem zpow {α} {l : Filter α} {f : α → G} {x : G} (hf : Tendsto f l (𝓝 x)) (z : ℤ) :
    Tendsto (fun x => f x ^ z) l (𝓝 (x ^ z)) :=
  (continuousAt_zpow _ _).tendsto.comp hf

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