to_localInverse — Mathlib

English

The local inverse is itself a ContDiffAt function.

Русский

Локальная обратная функция сама по себе является ContDiffAt.

LaTeX

$$$\text{ContDiffAt } 𝕂 n (\text{hf.localInverse hf' hn}) (f a)$$$

Lean4

/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible derivative
at `a`, the inverse function (produced by `ContDiff.toOpenPartialHomeomorph`) is
also `ContDiff`. -/
theorem to_localInverse (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) :
    ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a) :=
  by
  have := hf.localInverse_apply_image hf' hn
  apply (hf.toOpenPartialHomeomorph f hf' hn).contDiffAt_symm (image_mem_toOpenPartialHomeomorph_target hf hf' hn)
  · convert hf'
  · convert hf

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