const_cpow — Mathlib

English

If f,g are continuous and f(a) lies in the slit plane for all a, then the function x ↦ f(x)^g(x) is continuous.

Русский

Если f,g непрерывны и f(a) ∈ slitPlane для всех a, то f(x)^g(x) непрерывно по x.

LaTeX

$$$$\\text{If } f,g:\\, \n\\alpha \\to \\mathbb{C},\\ f,g\\text{ continuous},\\ \\forall a, f(a) \\in \\text{slitPlane} \Rightarrow x \\mapsto f(x)^{g(x)} \\text{ is continuous}. $$$$

Lean4

nonrec theorem const_cpow {b : ℂ} (hf : ContinuousAt f a) (h : b ≠ 0 ∨ f a ≠ 0) : ContinuousAt (fun x => b ^ f x) a :=
  hf.const_cpow h

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