pow — Mathlib

English

If f is continuous within a set s at x, then f^n is continuous within s at x for every n.

Русский

Если f непрерывна внутри множества s в точке x, то f^n непрерывна внутри s в x для каждого n.

LaTeX

$$$\\text{ContinuousWithinAt } f s x \\Rightarrow \\forall n,\\ \\text{ContinuousWithinAt } (\\lambda x, f(x)^n) s x$$$

Lean4

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

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