English
If f0 and f1 agree in a neighborhood of x within s and f0 x = f1 x, then HasLineDerivWithinAt for f0 equals HasLineDerivWithinAt for f1 on s.
Русский
Если f0 и f1 совпадают в окрестности x внутри s и значения в x совпадают, то линейная производная внутри s совпадает для f0 и f1.
LaTeX
$$$(nhdsWithin x s).EventuallyEq f_{0} f_{1} \\Rightarrow f_{0}(x)=f_{1}(x) \\Rightarrow \\mathrm{HasLineDerivWithinAt}_{\\mathbb{K}}(f_{0},f',s,x,v) \\iff \\mathrm{HasLineDerivWithinAt}_{\\mathbb{K}}(f_{1},f',s,x,v)$$$
Lean4
theorem hasLineDerivWithinAt_iff (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : f₀ x = f₁ x) :
HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v :=
by
apply hasDerivWithinAt_iff
· have A : Continuous (fun (t : 𝕜) ↦ x + t • v) := by fun_prop
exact A.continuousWithinAt.preimage_mem_nhdsWithin'' h (by simp)
· simpa using hx
