hasFDerivAt_polarCoordReal_symm — Mathlib

English

HasFDerivAt for polarCoordReal.symm at x exists with the described derivative.

Русский

Для polarCoordReal.symm в точке x существует производная с указанным дифференциалом.

LaTeX

$$$\\text{HasFDerivAt}(\\text{polarCoordReal}(K).symm, FDerivPolarCoordRealSymm(K)(x), x)$$$

Lean4

theorem hasFDerivAt_polarCoordReal_symm (x : realMixedSpace K) :
    HasFDerivAt (polarCoordReal K).symm (FDerivPolarCoordRealSymm K x) x := by
  classical exact (hasFDerivAt_id x.1).prodMap x (hasFDerivAt_pi_polarCoord_symm x.2)

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