English
Complex composition properties of toOpenPartialHomeomorph mirror the base function with inverse derivative data.
Русский
Свойства композиции toOpenPartialHomeomorph сохраняют базовую функцию с данными обратной производной.
LaTeX
$$$\text{toOpenPartialHomeomorph } f \text{ isomorphism on appropriate domains}$$$
Lean4
/-- Given a function with an invertible strict derivative at `a`, returns an `OpenPartialHomeomorph`
with `to_fun = f` and `a ∈ source`. This is a part of the inverse function theorem.
The other part `HasStrictFDerivAt.to_localInverse` states that the inverse function
of this `OpenPartialHomeomorph` has derivative `f'.symm`. -/
def toOpenPartialHomeomorph (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : OpenPartialHomeomorph E F :=
ApproximatesLinearOn.toOpenPartialHomeomorph f (Classical.choose hf.approximates_deriv_on_open_nhds)
(Classical.choose_spec hf.approximates_deriv_on_open_nhds).2.2
(f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => NNReal.half_lt_self <| ne_of_gt <| inv_pos.2 hf')
(Classical.choose_spec hf.approximates_deriv_on_open_nhds).2.1
