Solution (source code)

= Solution

The <function> $f$ is <differentiable> at $x_0$ if there exists a finite real number $L$ such that
$$
\boxed{\forall\varepsilon>0\ \exists\delta>0\ \forall x\in\mathbb R:
\quad 0<|x-x_0|<\delta\ \Longrightarrow\
\left|\frac{f(x)-f(x_0)}{x-x_0}-L\right|<\varepsilon}.
$$
Then $f'(x_0)=L$. The puncture $0<|x-x_0|$ makes the <difference quotient> defined; requiring a finite real $L$ distinguishes an ordinary <derivative> from an infinite slope.