pow — Mathlib

English

For any f: X → M and any x ∈ X, if f is continuous at x, then f^n is continuous at x for every n.

Русский

Для любого f: X → M и точки x, если f непрерывна в x, то f^n непрерывна в x для каждого n.

LaTeX

$$$\\text{ContinuousAt } f x \\Rightarrow \\forall n, \\text{ContinuousAt } (\\lambda y, f(y)^n) x$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem pow {f : X → M} {x : X} (hf : ContinuousAt f x) (n : ℕ) : ContinuousAt (fun x => f x ^ n) x :=
  Filter.Tendsto.pow hf n

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