zpow₀ — Mathlib

English

If f is continuous at a, then f(x)^m is continuous at a for all m ∈ ℤ provided a ≠ 0 or m ≥ 0.

Русский

Если f непрерывна в точке a, тогда f(x)^m непрерывна в a для всех m ∈ ℤ при условии a ≠ 0 или m ≥ 0.

LaTeX

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

Lean4

@[fun_prop]
nonrec theorem zpow₀ (hf : ContinuousAt f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) : ContinuousAt (fun x => f x ^ m) a :=
  hf.zpow₀ m h

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