English
Let 𝕜 be a nontrivial normed field, E and F normed spaces over 𝕜. If two functions f and f1 from E to F agree in a neighborhood of x within a set s, and t is a subset of s, then the derivative within t of f1 at every point in the nhdsWithin x s agrees (eventually) with the derivative within t of f. Equivalently, f1 =ᶠ[𝓝[s] x] f implies fderivWithin 𝕜 f1 t =ᶠ[𝓝[s] x] fderivWithin 𝕜 f t, provided t ⊆ s.
Русский
Пусть 𝕜 — неслабо нормированное поле, E и F — нормированные пространства над 𝕜. Если две функции f и f1 из E в F совпадают в окрестности точки x внутри множества s, и т⊆s, то локальная производная по f1 на область t совпадает (почти повсюду) с локальной производной по f на t около x.
LaTeX
$$$ fderivWithin \ 𝕜 \ f_1 \ t =^f_{\mathcal N_s(x)} fderivWithin \ 𝕜 \ f \ t \quad\text{при} \ t \subseteq s \\ f_1 =^f_{\mathcal N_s(x)} f$$$
Lean4
theorem fderivWithin' (hs : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) : fderivWithin 𝕜 f₁ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 f t :=
(eventually_eventually_nhdsWithin.2 hs).mp <|
eventually_mem_nhdsWithin.mono fun _y hys hs =>
EventuallyEq.fderivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht) (hs.self_of_nhdsWithin hys)
