cpow — Mathlib

English

If f,g are ContinuousWithinAt on s and f(a) lies in the slit plane for all a ∈ s, then f(x)^g(x) is ContinuousWithinAt on s at a.

Русский

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

LaTeX

$$$$\\text{If } f,g:\\, \\alpha \\to \\mathbb{C},\\ s\\subseteq \\alpha,\\ a\\in s,\\ (f,g)\\text{ ContinuousWithinAt on } s,\\ f(a) \\in \\text{slitPlane} \\Rightarrow \\text{ContinuousWithinAt}(x\\mapsto f(x)^{g(x)})s a.$$$$

Lean4

nonrec theorem cpow (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) (h0 : f a ∈ slitPlane) :
    ContinuousWithinAt (fun x => f x ^ g x) s a :=
  hf.cpow hg h0

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