English
If f0 and f1 are eventually equal on nhds within s at x, and f0 x = f1 x, then LineDifferentiableWithinAt for f0 equals that for f1 on s at x in direction v.
Русский
Если 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{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{0},s;x,v) \\iff \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{1},s;x,v)$$$
Lean4
theorem lineDifferentiableWithinAt_iff (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : f₀ x = f₁ x) :
LineDifferentiableWithinAt 𝕜 f₀ s x v ↔ LineDifferentiableWithinAt 𝕜 f₁ s x v :=
⟨fun h' ↦ ((h.hasLineDerivWithinAt_iff hx).1 h'.hasLineDerivWithinAt).lineDifferentiableWithinAt, fun h' ↦
((h.hasLineDerivWithinAt_iff hx).2 h'.hasLineDerivWithinAt).lineDifferentiableWithinAt⟩
