hasFDerivAt_of_restrictScalars — Mathlib

English

If HasFDerivAt f g′ x holds and f′.restrictScalars 𝕜 = g′, then HasFDerivAt f f′ x follows. The differentiability data transfers from 𝕜′-to 𝕜-scalar structure at a point.

Русский

Если существует HasFDerivAt f g′ в точке x для 𝕜′ и f′.restrictScalars 𝕜 = g′, то имеет место HasFDerivAt f f′ x. Таким образом, дифференцируемость перенесена через ограничение скаляров.

LaTeX

$$$\\text{HasFDerivAt } f g'\\, x \\wedge f'.\\restrictScalars 𝕜 = g' \\Rightarrow \\text{HasFDerivAt } f f'\\, x$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivAt f g' x) (H : f'.restrictScalars 𝕜 = g') :
    HasFDerivAt f f' x := by
  rw [← H] at h
  exact .of_isLittleO h.isLittleO

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