English
If a real function f has derivatives at every point y ≠ x given by g(y), and f and g are continuous at x, then f is differentiable at x with derivative g(x).
Русский
Если функция f имеет производную в каждой точке y ≠ x, равную g(y), и f, g непрерывны в x, тогда f дифференцируема в x и производная равна g(x).
LaTeX
$$$$ \\text{HasDerivAt } f (g(x)) x, \\quad \\text{with } g(y) \\text{ for } y \\neq x, \\text{ and } f,g \\text{ continuous at } x. $$$$
Lean4
/-- If a real function `f` has a derivative `g` everywhere but at a point, and `f` and `g` are
continuous at this point, then `g` is the derivative of `f` everywhere. -/
theorem hasDerivAt_of_hasDerivAt_of_ne' {f g : ℝ → E} {x : ℝ} (f_diff : ∀ y ≠ x, HasDerivAt f (g y) y)
(hf : ContinuousAt f x) (hg : ContinuousAt g x) (y : ℝ) : HasDerivAt f (g y) y :=
by
rcases eq_or_ne y x with (rfl | hne)
· exact hasDerivAt_of_hasDerivAt_of_ne f_diff hf hg
· exact f_diff y hne
