pow — Mathlib

English

If f tends to x along a filter l, then f^n tends to x^n along l, for any n ∈ ℕ.

Русский

Если f стремится к x вдоль фильтра l, то f^n стремится к x^n вдоль l для любого n ∈ ℕ.

LaTeX

$$$\\text{If } f : \\alpha \\to M\\text{ and } l \\ text{ is a filter with } f \\to x, \\text{ then } (a \\mapsto f(a)^n) \\to x^n$ in the corresponding nhds.$$

Lean4

@[to_additive]
theorem pow {l : Filter α} {f : α → M} {x : M} (hf : Tendsto f l (𝓝 x)) (n : ℕ) :
    Tendsto (fun x => f x ^ n) l (𝓝 (x ^ n)) :=
  (continuousAt_pow _ _).tendsto.comp hf

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