English
Let 𝕜 and 𝕜′ be nontrivially normed fields with a scalar tower 𝕜 → 𝕜′ acting on a normed algebra of E over 𝕜 and F over 𝕜. If a function f: E → F is differentiable with respect to 𝕜′, then f is differentiable with respect to 𝕜.
Русский
Пусть 𝕜 и 𝕜′ — ненулевые нормованные поля, имеющие на E и F структуру в виде 𝕜′-модулей над 𝕜 и 𝕜′ соответствующих векторов, образующая цепь 𝕜 → 𝕜′. Если f: E → F дифференцируема по 𝕜′, то она дифференцируема и по 𝕜.
LaTeX
$$$\\forall 𝕜 \\; [\\text{NontriviallyNormedField } 𝕜],\\; {𝕜'}\\; [\\text{NontriviallyNormedField } 𝕜'],\\; {E} , {F},\\; {f : E \\to F},\\; h: \\text{Differentiable}_{𝕜'}(f) \\;\\Rightarrow\\; \\text{Differentiable}_{𝕜}(f).$$$
Lean4
@[fun_prop]
theorem restrictScalars (h : Differentiable 𝕜' f) : Differentiable 𝕜 f := fun x => (h x).restrictScalars 𝕜
