hasFDerivAt_pi_polarCoord_symm — Mathlib

English

For a finite index type ι, the derivative of the map x ↦ polarCoord.symm(x_i) exists componentwise and equals the expected Pi-assembled derivative.

Русский

Существует производная по каждой координате в пространстве Пи; производная x ↦ polarCoord.symm(x_i) равна ожидаемому компонентному произведению.

LaTeX

$$$HasFDerivAt\bigl( x \mapsto polarCoord.symm(x_i) \bigr)\bigl( fderivPiPolarCoordSymm(p)\bigr)\; p.$$$

Lean4

theorem hasFDerivAt_pi_polarCoord_symm (p : ι → ℝ × ℝ) :
    HasFDerivAt (fun x i ↦ polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p :=
  by
  rw [fderivPiPolarCoordSymm, hasFDerivAt_pi]
  exact fun i ↦ HasFDerivAt.comp _ (hasFDerivAt_polarCoord_symm _) (hasFDerivAt_apply i _)

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