zpow — Mathlib

English

For any f: α → G and any set s ⊆ α, and z ∈ ℤ, the map x ↦ f(x)^z is continuous on s whenever f is continuous on s.

Русский

Для любого f: α → G, подмножества s, и z ∈ ℤ, отображение x ↦ f(x)^z непрерывно на s, если f непрерывна на s.

LaTeX

$$$\forall f:\alpha \to G, \forall s, \text{ContinuousOn } f s \Rightarrow \forall z, \text{ContinuousOn}(x\mapsto f(x)^{z}) s.$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem zpow {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (fun x => f x ^ z) s := fun x hx =>
  (hf x hx).zpow z

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