# Extending differentiability to the boundary #

We investigate how differentiable functions inside a set extend to differentiable functions
on the boundary. For this, it suffices that the function and its derivative admit limits there.
A general version of this statement is given in `has_fderiv_at_boundary_of_tendsto_fderiv`

.

One-dimensional versions, in which one wants to obtain differentiability at the left endpoint or
the right endpoint of an interval, are given in
`has_deriv_at_interval_left_endpoint_of_tendsto_deriv`

and
`has_deriv_at_interval_right_endpoint_of_tendsto_deriv`

. These versions are formulated in terms
of the one-dimensional derivative `deriv ℝ f`

.

If a function `f`

is differentiable in a convex open set and continuous on its closure, and its
derivative converges to a limit `f'`

at a point on the boundary, then `f`

is differentiable there
with derivative `f'`

.

If a function is differentiable on the right of a point `a : ℝ`

, continuous at `a`

, and
its derivative also converges at `a`

, then `f`

is differentiable on the right at `a`

.

If a function is differentiable on the left of a point `a : ℝ`

, continuous at `a`

, and
its derivative also converges at `a`

, then `f`

is differentiable on the left at `a`

.

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 also the derivative of `f`

at this point.

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.