English
If two sets s and t agree in a neighborhood of x, then the property of being line-differentiable of f at x in the direction v with respect to s equals that with respect to t.
Русский
Если множества s и t совпадают в окрестности точки x, то свойство линейной дифференцируемости функции f в точке x по направлению v при учёте множества s эквивалентно такому свойству при учёте множества t.
LaTeX
$$$s =_{\\mathcal{N}(x)} t \\Rightarrow \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f;s;x,v) \\iff \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f;t;x,v)$$$
Lean4
theorem lineDifferentiableWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
LineDifferentiableWithinAt 𝕜 f s x v ↔ LineDifferentiableWithinAt 𝕜 f t x v :=
⟨fun h' ↦ ((hasLineDerivWithinAt_congr_set h).1 h'.hasLineDerivWithinAt).lineDifferentiableWithinAt, fun h' ↦
((hasLineDerivWithinAt_congr_set h.symm).1 h'.hasLineDerivWithinAt).lineDifferentiableWithinAt⟩
