The Dini-derivative criterion is the extended-real shadow of the library's finite derivative convention

The library's published notion of derivative, The derivative $f^{\mathrm{\prime }}(c)={\lim }_{x\to c}\frac{f(x)-f(c)}{x-c}$ of $f:A\to \mathbb{R}$ at a point $c\in A$ that is a limit point of $A$, and differentiability on a set, is a finite real number. For a function on an interval at an interior point, The four Dini derivatives always exist in the extended reals, satisfy the one-sided order inequalities, and detect finite differentiability says that the derivative exists exactly when the upper and lower right and left Dini derivatives all agree and their common value is finite. At an interval endpoint, the relative-domain derivative may exist while the two Dini derivatives on the unavailable side are not defined.

The extended-real cases are deliberately kept outside the word "derivative" in this library. If all four Dini derivatives agree at $+\mathrm{\infty }$ or at $-\mathrm{\infty }$, that is still informative, but it is not recorded as "$f^{\mathrm{\prime }}(x)$ exists" because the finite-value contract of The derivative $f^{\mathrm{\prime }}(c)={\lim }_{x\to c}\frac{f(x)-f(c)}{x-c}$ of $f:A\to \mathbb{R}$ at a point $c\in A$ that is a limit point of $A$, and differentiability on a set would then be false.