inv — Mathlib

English

If f is analytic within s and never vanishes on s, then the reciprocal map is analytic within s.

Русский

Если f аналитична внутри s и нигде на s не равна нулю, то обратная функция аналитична внутри s.

LaTeX

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

Lean4

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

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