const_cpow — Mathlib

English

If f is ContinuousOn on s and for all a ∈ s, f(a) ∈ slitPlane, then the function 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 : ContinuousOn f s) (h : b ≠ 0 ∨ ∀ a ∈ s, f a ≠ 0) : ContinuousOn (fun x => b ^ f x) s :=
  fun a ha => (hf a ha).const_cpow (h.imp id fun h => h a ha)

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