localInverse — Mathlib

English

If f is ContDiff and has an invertible derivative at a, then there exists a local inverse with the same regularity at f(a).

Русский

Если f имеет непрерывную производную в точке a и она обратно инвертируемая, существует локальная обратная функция с той же гладкостью в точке f(a).

LaTeX

$$$\text{ContDiffAt } 𝕂 n f a \wedge HasFDerivAt\ f\ (f' : E \to F) a \Rightarrow \text{ContDiffAt } 𝕂 n (\text{localInverse } f' ) (f a)$$$

Lean4

/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible derivative
at `a`, returns a function that is locally inverse to `f`. -/
def localInverse (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) : F → E :=
  (hf.hasStrictFDerivAt' hf' hn).localInverse f f' a

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