map_implicitFunction_eq — Mathlib

English

There is a canonical map to the implicit function from HasStrictFDerivAt, giving a derivative of the implicit function with kernel restriction.

Русский

Существует каноническое отображение к неявной функции из HasStrictFDerivAt, задающее производную неявной функции в ограничении ядра.

LaTeX

$$$ hf.to_implicitFunction hf' hker : HasStrictFDerivAt (hf.implicitFunction f f' hf' hker (f a)) (\ker f').subtypeL 0 $$$

Lean4

/-- `HasStrictFDerivAt.implicitFunction` sends `(z, y)` to a point in `f ⁻¹' z`. -/
theorem map_implicitFunction_eq (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
    ∀ᶠ p : F × ker f' in 𝓝 (f a, 0), f (hf.implicitFunction f f' hf' p.1 p.2) = p.1 :=
  haveI := FiniteDimensional.complete 𝕜 F
  map_implicitFunctionOfComplemented_eq ..

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