\begin{definition}[Definition:Extended Real Subtraction]
Let $\overline \R$ denote the extended real numbers.
Define '''extended real subtraction''' or '''subtraction on $\overline \R$''', denoted $-_{\overline \R}: \overline \R \times \overline \R \to \overline \R$, by:
:$\forall x, y \in \R: x -_{\overline \R} y := x -_{\R} y$ where $-_\R$ denotes real subtraction
:$\forall x \in \R: x -_{\overline \R} \paren {+\infty} = \paren {-\infty} -_{\overline \R} x := -\infty$
:$\forall x \in \R: x -_{\overline \R} \paren {-\infty} = \paren {+\infty} -_{\overline \R} x := +\infty$
:$\paren {-\infty} -_{\overline \R} \paren {+\infty} := -\infty$
:$\paren {+\infty} -_{\overline \R} \paren {-\infty} := +\infty$
In particular, the expressions:
:$\paren {+\infty} -_{\overline \R} \paren {+\infty}$
:$\paren {-\infty} -_{\overline \R} \paren {-\infty}$
are considered '''void''' and should be avoided.
When no danger of confusion arises, $-_{\overline \R}$ is usually replaced with the more familiar $-$.
From the definition of $-_{\overline \R}$ on bona fide real numbers, the name '''extended real subtraction''' is appropriate: the operation of real subtraction is indeed extended.
\end{definition}