cpow — Mathlib

English

If f and g are continuous and f(a) ∈ slitPlane for all a, then x ↦ f(x)^g(x) is continuous.

Русский

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

LaTeX

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

Lean4

theorem cpow (hf : Continuous f) (hg : Continuous g) (h0 : ∀ a, f a ∈ slitPlane) : Continuous fun x => f x ^ g x :=
  continuous_iff_continuousAt.2 fun a => hf.continuousAt.cpow hg.continuousAt (h0 a)

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