cpow — Mathlib

English

If fa and ga are analytic within a set and f avoids the slit on that set, then f^g is analytic within the set.

Русский

Если fa и ga аналитичны внутри множества, и f избегает разреза на этом множестве, то f^g аналитична внутри множества.

LaTeX

$$$\\text{AnalyticWithinAt}(\\,f^g\,)$ given fa analytic, ga analytic, and m: f(x)∈slitPlane$$

Lean4

/-- `f z ^ g z` is analytic if `f z` is not a nonpositive real -/
@[fun_prop]
theorem cpow (fa : AnalyticAt ℂ f x) (ga : AnalyticAt ℂ g x) (m : f x ∈ slitPlane) :
    AnalyticAt ℂ (fun z ↦ f z ^ g z) x :=
  by
  rw [← analyticWithinAt_univ] at fa ga ⊢
  exact fa.cpow ga m

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