hasStrictFDerivAt — Mathlib

English

If a function is analytic at a point and has an invertible derivative, then its inverse is analytic at the image point.

Русский

Если функция аналитична в точке и производная обратима, то ее обратное отображение аналитично в точке образа.

LaTeX

$$$\text{analyticAt_symm} (f) \Rightarrow \text{AnalyticAt 𝕜 f.symm } (f a)$$$

Lean4

theorem hasStrictFDerivAt (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) :
    HasStrictFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1)) (x + y) :=
  (h.changeOrigin hy).toHasFPowerSeriesOnBall.hasFPowerSeriesAt.hasStrictFDerivAt

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