implicitFunction_hasStrictFDerivAt

English

A reiterated version of the nhds equality for left-hand map under the implicit function data.

Русский

Повторная версия равенства nhds при отображении слева для данных неявной функции.

LaTeX

$$map φ.leftFun (𝓝 φ.pt) = 𝓝 (φ.leftFun φ.pt)$$

Lean4

theorem implicitFunction_hasStrictFDerivAt (g'inv : G →L[𝕜] E)
    (hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G) (hg'invf : φ.leftDeriv.comp g'inv = 0) :
    HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt) :=
  by
  have := φ.hasStrictFDerivAt.to_localInverse
  simp only [prodFun] at this
  convert this.comp (φ.rightFun φ.pt) ((hasStrictFDerivAt_const _ _).prodMk (hasStrictFDerivAt_id _))
  simp only [ContinuousLinearMap.ext_iff, ContinuousLinearMap.comp_apply] at hg'inv hg'invf ⊢
  simp [ContinuousLinearEquiv.eq_symm_apply, *]

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