fderiv_restrictScalars — Mathlib

English

If DifferentiableAt 𝕜′ f x holds, then fderiv 𝕜 f x equals the 𝕜-restriction of fderiv 𝕜′ f x: fderiv 𝕜 f x = (fderiv 𝕜′ f x).restrictScalars 𝕜.

Русский

Пусть f дифференцируема в точке x относительно 𝕜′, тогда дифференциал f по 𝕜 равен ограничению по скалярам от дифференциала по 𝕜′: fderiv 𝕜 f x = (fderiv 𝕜′ f x).restrictScalars 𝕜.

LaTeX

$$$fderiv 𝕜 f x = (fderiv 𝕜' f x).restrictScalars 𝕜$$$

Lean4

theorem fderiv_restrictScalars (h : DifferentiableAt 𝕜' f x) : fderiv 𝕜 f x = (fderiv 𝕜' f x).restrictScalars 𝕜 :=
  (h.hasFDerivAt.restrictScalars 𝕜).fderiv

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