English
For a function f: ℂ → E and a neighborhood basis, differentiability on s \ {c} together with continuity at c is equivalent to differentiability on s.
Русский
Для функции f: ℂ → E существование дифференцируемости на s \ {c} вместе с непрерывностью в c эквивалентно существованию дифференцируемости на s.
LaTeX
$$$\\displaystyle \\text{Diffe(rentiableOn) on }(s\\setminus\\{c\\})\\land ContinuousAt f c \\iff DifferentiableOn f s.$$$
Lean4
theorem differentiableOn_compl_singleton_and_continuousAt_iff {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hs : s ∈ 𝓝 c) :
DifferentiableOn ℂ f (s \ { c }) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s :=
by
refine ⟨?_, fun hd => ⟨hd.mono diff_subset, (hd.differentiableAt hs).continuousAt⟩⟩
rintro ⟨hd, hc⟩ x hx
rcases eq_or_ne x c with (rfl | hne)
· refine
(analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ hc).differentiableAt.differentiableWithinAt
refine eventually_nhdsWithin_iff.2 ((eventually_mem_nhds_iff.2 hs).mono fun z hz hzx => ?_)
exact hd.differentiableAt (inter_mem hz (isOpen_ne.mem_nhds hzx))
· simpa only [DifferentiableWithinAt, HasFDerivWithinAt, hne.nhdsWithin_diff_singleton] using hd x ⟨hx, hne⟩
