zpow₀ — Mathlib

English

If f is continuous on s, then for all m ∈ ℤ and all a ∈ s with f(a) ≠ 0 or 0 ≤ m, the map x ↦ f(x)^m is continuous on s.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem zpow₀ (hf : ContinuousOn f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) : ContinuousOn (fun x => f x ^ m) s :=
  fun a ha => (hf a ha).zpow₀ m (h a ha)

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