ThmDex – An index of mathematical definitions, results, and conjectures.
Result R3583 on D4381: Random basic number
Random basic number absolutisation equals sum of positive and negative parts
Formulation 0
Let $X \in \text{Random} [-\infty, \infty]$ be a D4381: Random basic number such that
(i) $X^+$ is the D1289: Basic function positive part of $X$
(ii) $X^-$ is the D1290: Basic function negative part of $X$
Then \begin{equation} |X| = X^+ + X^- \end{equation}
Proofs
Proof 0
Let $X \in \text{Random} [-\infty, \infty]$ be a D4381: Random basic number such that
(i) $X^+$ is the D1289: Basic function positive part of $X$
(ii) $X^-$ is the D1290: Basic function negative part of $X$