English
If HasFDerivWithinAt f g′ s x holds and f′.restrictScalars 𝕜 = g′, then HasFDerivWithinAt f f′ s x follows. In words, the 𝕜′-derivative determines the 𝕜-derivative when restricted scalars agree.
Русский
Если существует локальная производная HasFDerivWithinAt f g′ на s в точке x и f′.restrictScalars 𝕜 = g′, тогда существует локальная производная HasFDerivWithinAt f f′ на s в x. Иначе говоря, производная по 𝕜-действительно следует из производной по 𝕜′ при согласовании ограничений скаляров.
LaTeX
$$$\\text{HasFDerivWithinAt } f g'\\, s\\, x \\quad \\land\\quad f'.\\restrictScalars 𝕜 = g' \\;\\Rightarrow\\; \\text{HasFDerivWithinAt } f f'\\, s\\, x$$$
Lean4
@[fun_prop]
theorem of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivWithinAt f g' s x) (H : f'.restrictScalars 𝕜 = g') :
HasFDerivWithinAt f f' s x := by
rw [← H] at h
exact .of_isLittleO h.isLittleO
