to_implicitFunction — Mathlib

English

On the domain of f a, the open partial homeomorphism sends a to (f a, 0).

Русский

На области определения f часть открытого частичного гомоморфизма отправляет a в (f(a), 0).

LaTeX

$$$ hf.implicitToOpenPartialHomeomorph f f' hf' a = (f a, 0) $$$

Lean4

theorem to_implicitFunction (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
    HasStrictFDerivAt (hf.implicitFunction f f' hf' (f a)) (ker f').subtypeL 0 :=
  haveI := FiniteDimensional.complete 𝕜 F
  to_implicitFunctionOfComplemented ..

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