English
For a ≠ b, differentiableWithinAt dslope f a on s at b is equivalent to differentiableWithinAt f on s at b.
Русский
Для a ≠ b, DifferentiableWithinAt dslope f a на s в b эквивалентно DifferentiableWithinAt f на s в b.
LaTeX
$$$\text{DifferentiableWithinAt}( dslope\ f\ a, s, b) \iff \text{DifferentiableWithinAt}( f, s, b) \quad (b \neq a)$$$
Lean4
theorem differentiableWithinAt_dslope_of_ne (h : b ≠ a) :
DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b :=
by
refine ⟨DifferentiableWithinAt.of_dslope, fun hd => ?_⟩
refine
(((differentiableWithinAt_id.sub_const a).inv (sub_ne_zero.2 h)).smul (hd.sub_const (f a))).congr_of_eventuallyEq ?_
(dslope_of_ne _ h)
refine (eqOn_dslope_slope _ _).eventuallyEq_of_mem ?_
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)
