ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Binary endorelation
Preordering relation
Partial ordering relation
Ordering relation
Ordered set
Map truncation
Definition D1289
Basic function positive part
Formulation 1
Let $f : X \to [-\infty, \infty]$ be a D3180: Basic function.
The positive part of $f$ is the D3180: Basic function \begin{equation} f^+ : X \to [-\infty, \infty], \quad f^+(x) = \max(f(x), 0) \end{equation}
Results
R3518: Partition of random basic number into positive and negative parts