zpow — Mathlib

English

For any f: α → G and any x ∈ α, and z ∈ ℤ, the map a ↦ a^z is continuous at x whenever f is continuous at x.

Русский

Для любого f: α → G, точки x и z ∈ ℤ, отображение a ↦ a^z непрерывно в x, если f непрерывна в x.

LaTeX

$$$\forall f:\alpha \to G, \forall x:\alpha, \forall z:\mathbb{Z}, \text{ContinuousAt}(a\mapsto a^{z}, x).$$$

Lean4

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

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