fun_zpow — Mathlib

English

For nhd analytic f, if f(z) ≠ 0, then f(z)^{-1} is analytic in nhd.

Русский

Для аналитической функции f на nhd, если f(z) ≠ 0, то f(z)^{-1} аналитично в nhd.

LaTeX

$$AnalyticOnNhd 𝕜 f s → (∀ z ∈ s, f z ≠ 0) → AnalyticOnNhd 𝕜 f^{-1} s$$

Lean4

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
theorem fun_zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOn 𝕜 f s) (h₂f : ∀ z ∈ s, f z ≠ 0) :
    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s := fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)

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