const_cpow — Mathlib

English

If f is ContinuousOn on s and for all a ∈ s, f(a) ∈ slitPlane, then the map x ↦ b^{f(x)} is ContinuousOn on s.

Русский

Если f непрерывна на s и f(a) ∈ slitPlane для каждого a ∈ s, то x ↦ b^{f(x)} непрерывна на s.

LaTeX

$$$$\\text{If } f:\\, s \\to \\mathbb{C},\\ ContinuousOn\\ f\\ s,\\ \\forall a\\in s,\\ f(a) \\in \\text{slitPlane} \\Rightarrow \\text{ContinuousOn } (x\\mapsto b^{f(x)})\\ s.$$$$

Lean4

theorem const_cpow {b : ℂ} (hf : Continuous f) (h : b ≠ 0 ∨ ∀ a, f a ≠ 0) : Continuous fun x => b ^ f x :=
  continuous_iff_continuousAt.2 fun a => hf.continuousAt.const_cpow <| h.imp id fun h => h a

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