inv — Mathlib

English

Given analytic f and nonvanishing on the domain, the map x ↦ f(x)^{-1} is analytic inside the domain.

Русский

Дано аналитическое f и не обращающееся в ноль на области отображение x ↦ f(x)^{−1} аналитично внутри области.

LaTeX

$$AnalyticWithinAt 𝕜 f s x → Ne (f x) 0 → AnalyticWithinAt 𝕜 (f^{-1}) s x$$

Lean4

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem inv {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x) (f0 : f x ≠ 0) :
    AnalyticWithinAt 𝕜 f⁻¹ s x :=
  fun_inv fa f0

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