differentiableAt_iff_restrictScalars

English

For differentiable at x with respect to 𝕜, there is an equivalence between differentiability at 𝕜′ and the existence of a 𝕜′-derivative that restricts to the 𝕜-derivative.

Русский

Для дифференцируемости в точке x относительно 𝕜 существует эквивалентность между дифференцируемостью по 𝕜′ и существованием 𝕜′-производной, которая ограничивается до 𝕜-производной.

LaTeX

$$DifferentiableAt 𝕜 f x → (DifferentiableAt 𝕜' f x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderiv 𝕜 f x)$$

Lean4

theorem differentiableAt_iff_restrictScalars (hf : DifferentiableAt 𝕜 f x) :
    DifferentiableAt 𝕜' f x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderiv 𝕜 f x :=
  by
  rw [← differentiableWithinAt_univ, ← fderivWithin_univ]
  exact differentiableWithinAt_iff_restrictScalars 𝕜 hf.differentiableWithinAt uniqueDiffWithinAt_univ

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