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

Result R5300 on D1747: Unsigned basic integral

Unsigned basic integral over an empty set equals zero

Formulation 0

Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that

(1)	$f : X \to [0, \infty]$ is a D313: Measurable function on $M$

Then \begin{equation} \int_{\emptyset} f \, d \mu = 0 \end{equation}

Formulation 1

Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that

(1)	$f : X \to [0, \infty]$ is a D313: Measurable function on $M$

Then \begin{equation} \int_X I_{\emptyset} f \, d \mu = 0 \end{equation}

Proofs

Proof 0

Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that

(1)	$f : X \to [0, \infty]$ is a D313: Measurable function on $M$

Since $x \not\in \emptyset$ for all $x \in X$, then we have $I_{\emptyset}(x) f(x) = 0$ for all $x \in X$. Hence, applying result R3515: Unsigned basic integral zero iff function almost everywhere zero, we have \begin{equation} \int_{\emptyset} f \, d \mu = \int_X I_{\emptyset} f \, d \mu = 0 \end{equation} $\square$