English
If an open partial homeomorphism f is analytic at a point where a derivative exists, then its inverse is analytic at a.
Русский
Если открытое частичное гомоморфное отображение f аналитично в точке a, где существует производная, то его обратное отображение аналитично в a.
LaTeX
$$$\text{analyticAt_symm }(f) \Rightarrow \text{AnalyticAt } 𝕜 f^{-1} a$$$
Lean4
/-- If an open partial homeomorphism `f` is analytic at a point `f.symm a`, with invertible
derivative, then its inverse is analytic at `a`. -/
theorem analyticAt_symm (f : OpenPartialHomeomorph E F) {a : F} {i : E ≃L[𝕜] F} (h0 : a ∈ f.target)
(h : AnalyticAt 𝕜 f (f.symm a)) (h' : fderiv 𝕜 f (f.symm a) = i) : AnalyticAt 𝕜 f.symm a :=
by
have : a = f (f.symm a) := by simp [h0]
rw [this]
exact f.analyticAt_symm' (by simp [h0]) h h'
