zpow₀ — Mathlib

English

If f is globally continuous and the nonzero condition holds for all a, then the map x ↦ f(x)^m is continuous for each integer m.

Русский

Если f непрерывна на всём множестве и выполняется условие f(a) ≠ 0 или 0 ≤ m для всех a, то x ↦ f(x)^m непрерывна для каждого целого m.

LaTeX

$$$\\text{Continuous } f \\Rightarrow \\forall m:\\mathbb{Z},\\ (\\forall a, f(a) \\neq 0 \\lor 0 \\le m) \\Rightarrow \\text{Continuous }(x \\mapsto f(x)^{m})$$$

Lean4

@[continuity, fun_prop]
theorem zpow₀ (hf : Continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0 ∨ 0 ≤ m) : Continuous fun x => f x ^ m :=
  continuous_iff_continuousAt.2 fun x => (hf.tendsto x).zpow₀ m (h0 x)

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