restrictScalars_fderivWithin — Mathlib

English

Let hf be DifferentiableWithinAt 𝕜′ f s x and hs UniqueDiffWithinAt 𝕜 s x. Then (fderivWithin 𝕜′ f s x).restrictScalars 𝕜 = fderivWithin 𝕜 f s x.

Русский

Пусть hf = DifferentiableWithinAt 𝕜′ f s x и hs = UniqueDiffWithinAt 𝕜 s x. Тогда (fderivWithin 𝕜′ f s x).restrictScalars 𝕜 = fderivWithin 𝕜 f s x.

LaTeX

$$$\\bigl(fderivWithin 𝕜' f s x\\bigr).restrictScalars 𝕜 = fderivWithin 𝕜 f s x$$$

Lean4

theorem restrictScalars_fderivWithin (hf : DifferentiableWithinAt 𝕜' f s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
    (fderivWithin 𝕜' f s x).restrictScalars 𝕜 = fderivWithin 𝕜 f s x :=
  ((hf.hasFDerivWithinAt.restrictScalars 𝕜).fderivWithin hs).symm

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