zpow₀ — Mathlib

English

If f is continuous within at s at a, then f(x)^m is continuous within at a for all m, provided a satisfies the usual condition.

Русский

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

LaTeX

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

Lean4

nonrec theorem zpow₀ (hf : ContinuousWithinAt f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
    ContinuousWithinAt (fun x => f x ^ m) s a :=
  hf.zpow₀ m h

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