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

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$