implicitToOpenPartialHomeomorphOfComplemented_fst

English

Given a differentiable map f with surjective derivative f' and complemented kernel, one can form a data structure for an implicit function data with kernel as the target.

Русский

При задании дифференцируемой функции f с сюръективной производной и дополненным ядром ker f' можно образовать структуру данных для неявной функции с ядром как целью.

LaTeX

$$implicitFunctionDataOfComplemented (f) (f') (hf) (hf') (hker) : ImplicitFunctionData 𝕜 E F (ker f')$$

Lean4

@[simp]
theorem implicitToOpenPartialHomeomorphOfComplemented_fst (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
    (hker : (ker f').ClosedComplemented) (x : E) :
    (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker x).fst = f x :=
  rfl

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