zpow — Mathlib

English

If f is continuous within set s at x, then for every z ∈ ℤ, the map x ↦ f(x)^z is continuous within s at x.

Русский

Если f непрерывна внутри множества s в точке x, то для каждого z ∈ ℤ отображение x ↦ f(x)^z непрерывно в s в x.

LaTeX

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

Lean4

@[to_additive]
theorem zpow {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) :
    ContinuousWithinAt (fun x => f x ^ z) s x :=
  Filter.Tendsto.zpow hf z

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