ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4275 on D5480: Even real function

Absolute value function is an even basic real function

Formulation 0

Let $t \mapsto |t|$ be the D412: Absolute value function.
Let $x \in \mathbb{R}$ be a D993: Real number.

Then \begin{equation} |- x| = |x| \end{equation}