Inverse function theorem, C^r
case #
In this file we specialize the inverse function theorem to C^r
-smooth functions.
Given a ContDiff
function over 𝕂
(which is ℝ
or ℂ
) with an invertible
derivative at a
, returns an OpenPartialHomeomorph
with to_fun = f
and a ∈ source
.
Equations
Instances For
Alias of ContDiffAt.toOpenPartialHomeomorph
.
Given a ContDiff
function over 𝕂
(which is ℝ
or ℂ
) with an invertible
derivative at a
, returns an OpenPartialHomeomorph
with to_fun = f
and a ∈ source
.
Instances For
Alias of ContDiffAt.toOpenPartialHomeomorph_coe
.
Alias of ContDiffAt.image_mem_toOpenPartialHomeomorph_target
.
Given a ContDiff
function over 𝕂
(which is ℝ
or ℂ
) with an invertible derivative
at a
, returns a function that is locally inverse to f
.
Equations
- hf.localInverse hf' hn = HasStrictFDerivAt.localInverse f f' a ⋯
Instances For
Given a ContDiff
function over 𝕂
(which is ℝ
or ℂ
) with an invertible derivative
at a
, the inverse function (produced by ContDiff.toOpenPartialHomeomorph
) is
also ContDiff
.