to_local_left_inverse — Mathlib

English

The localInverse is defined as the inverse of the local open partial homeomorph.

Русский

Локальное обратное определяется как обратное локального открытого частичного гомоморфизма.

LaTeX

$$$ \operatorname{localInverse} (hf) = (hf.toOpenPartialHomeomorph f).symm $$$

Lean4

/-- If `f : E → F` has an invertible derivative `f'` at `a` in the sense of strict differentiability
and `g (f x) = x` in a neighborhood of `a`, then `g` has derivative `f'.symm` at `f a`.

For a version assuming `f (g y) = y` and continuity of `g` at `f a` but not `[CompleteSpace E]`
see `of_local_left_inverse`. -/
theorem to_local_left_inverse (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) {g : F → E}
    (hg : ∀ᶠ x in 𝓝 a, g (f x) = x) : HasStrictFDerivAt g (f'.symm : F →L[𝕜] E) (f a) :=
  hf.to_localInverse.congr_of_eventuallyEq <| (hf.localInverse_unique hg).mono fun _ => Eq.symm

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