fun_inv — Mathlib

English

If f is analytic at a point and never vanishes there, then the inverse map is analytic there.

Русский

Если функция аналитична в точке и не обращается в нуль в этой точке, то отображение инверсии аналитично в этой точке.

LaTeX

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

Lean4

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
@[fun_prop]
theorem fun_inv {f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : f x ≠ 0) : AnalyticAt 𝕜 (fun x ↦ (f x)⁻¹) x :=
  (analyticAt_inv f0).comp fa

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