English
If s and t are NHDS-equivalent near x, then line derivative within s at x in direction v equals line derivative within t at x in direction v.
Русский
Если множества s и t эквивалентны в окрестности точки x, то линейная производная внутри s в точке x по направлению v равна линейной производной внутри t в той же точке и направлении.
LaTeX
$$$s =_{\\mathcal{N}(x)} t \\Rightarrow \\mathrm{lineDerivWithin}_{\\mathbb{K}}(f;s;x,v) = \\mathrm{lineDerivWithin}_{\\mathbb{K}}(f;t;x,v)$$$
Lean4
theorem lineDerivWithin_congr_set (h : s =ᶠ[𝓝 x] t) : lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t x v :=
by
apply derivWithin_congr_set
let F := fun (t : 𝕜) ↦ x + t • v
have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
have : s =ᶠ[𝓝 (F 0)] t := by convert h; simp [F]
exact B.preimage_mem_nhds this
