pow — Mathlib

English

If f is continuous on a set s, then the map x ↦ f(x)^n is continuous on s for every n.

Русский

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

LaTeX

$$$\\forall n,\\; \\text{ContinuousOn } f s \\Rightarrow \\text{ContinuousOn } (\\lambda x, f(x)^n) s$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem pow {f : X → M} {s : Set X} (hf : ContinuousOn f s) (n : ℕ) : ContinuousOn (fun x => f x ^ n) s := fun x hx =>
  (hf x hx).pow n

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