Result on D41: Indicator function
Pointwise product with indicator function is lower bound for unsigned basic function
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}
Proofs
Proof 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$.
If $X$ is empty, the inequality $f(x) I_E(x) \leq f(x)$ holds vacuously for all $x \in X$, so assume that $X$ is nonempty and let $x \in X$. If $x \in X \setminus E$, then $f(x) I_E(x) = f(x) \leq f(x)$ holds trivially. If instead $x \in E$, then $f(x) I_E(x) = 0 \leq f(x)$ holds since $f$ is unsigned. $\square$