ThmDex – An index of mathematical definitions, results, and conjectures.
F8071
Formulation 0
Let $f : X \to [0, \infty]$ be an D4361: Unsigned basic function.
Let $I_E$ be an D41: Indicator function on $X$ for $E \subseteq X$.
Then \begin{equation} f I_E \leq f \end{equation}