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