fun_inv — Mathlib

English

If f is analytic on a set and is nonzero on that set, then f^{-1} is analytic on that set.

Русский

Если f аналитична на множестве и не равна нулю на этом множестве, то f^{-1} аналитична на этом множестве.

LaTeX

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

Lean4

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem fun_inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
    AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s := fun x m ↦ (fa x m).inv (f0 x m)

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