English
For hf DifferentiableWithinAt 𝕜 f s x and hs UniqueDiffWithinAt 𝕜 s x, DifferentiableWithinAt 𝕜' f s x holds iff there exists g' with g'.restrictScalars 𝕜 = fderivWithin 𝕜 f s x.
Русский
Для hf = DifferentiableWithinAt 𝕜 f s x и hs = UniqueDiffWithinAt 𝕜 s x, DifferentiableWithinAt 𝕜' f s x эквивалентно существованию g' с условием g'.restrictScalars 𝕜 = fderivWithin 𝕜 f s x.
LaTeX
$$DifferentiableWithinAt 𝕜' f s x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderivWithin 𝕜 f s x$$
Lean4
theorem differentiableWithinAt_iff_restrictScalars (hf : DifferentiableWithinAt 𝕜 f s x)
(hs : UniqueDiffWithinAt 𝕜 s x) :
DifferentiableWithinAt 𝕜' f s x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderivWithin 𝕜 f s x :=
by
constructor
· rintro ⟨g', hg'⟩
exact ⟨g', hs.eq (hg'.restrictScalars 𝕜) hf.hasFDerivWithinAt⟩
· rintro ⟨f', hf'⟩
exact ⟨f', hf.hasFDerivWithinAt.of_restrictScalars 𝕜 hf'⟩
