English
If s and t differ only on a set of x-neighborhood outside an exceptional point, derivative within are equivalent: HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x.
Русский
Если множества s и t отличаются только вне окрестности x, производная внутри совпадает: …
LaTeX
$$$HasFDerivWithinAt\\ f\\ f'\\ s\\ x \\Longrightarrow HasFDerivWithinAt\\ f\\ f'\\ t\\ x\\quad\\text{и наоборот при условии } s=ᶠ_{𝓝 x} t.$$$
Lean4
theorem hasFDerivWithinAt_congr_set' (y : E) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x :=
calc
HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' (s \ { y }) x := (hasFDerivWithinAt_diff_singleton _).symm
_ ↔ HasFDerivWithinAt f f' (t \ { y }) x :=
by
suffices 𝓝[s \ { y }] x = 𝓝[t \ { y }] x by simp only [HasFDerivWithinAt, this]
simpa only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter', diff_eq, inter_comm] using h
_ ↔ HasFDerivWithinAt f f' t x := hasFDerivWithinAt_diff_singleton _
