Differentiability away from finitely many exceptions

A function that is C^1 on a closed interval outside a finite exceptional set is differentiable at every interior point outside that set. In particular, it supplies a countable differentiability exception set for the interval.

theorem ContDiffOn.exists_countable_differentiableAt_of_finite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {s : Set ℝ} (h : ContDiffOn ℝ 1 f (Set.Icc a b \ s)) (hs : s.Finite) : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo a b \ S, DifferentiableAt ℝ f t

C^1 regularity outside a finite set supplies a countable differentiability exception set in the interior of the interval.