English
Let f, f1: E → F be functions between normed spaces over 𝕜, and s ⊆ E with x ∈ E. If f1 and f agree on a neighborhood of x within s (i.e., they coincide near x on s), then their derivatives within s at x are the same (as linear maps E → F).
Русский
Пусть f, f1: E → F — функции между нормированными пространствами над 𝕜, и s ⊆ E с x ∈ E. Если f1 и f совпадают на окрестности x внутри s, то их производные внутри s в точке x совпадают.
LaTeX
$$$\displaystyle \text{If } f_1 = f \text{ on a neighborhood of } x \text{ in } s, \text{ then } fderivWithin 𝕜 f_1 s = fderivWithin 𝕜 f s \text{ (as elements of } E \to^{} F).$$$
Lean4
protected theorem fderivWithin (hs : f₁ =ᶠ[𝓝[s] x] f) : fderivWithin 𝕜 f₁ s =ᶠ[𝓝[s] x] fderivWithin 𝕜 f s :=
hs.fderivWithin' Subset.rfl
