Lebesgue Integral of a Nonnegative Measurable Function

Let $(X,\mathcal{F},\mu)$ be a measure space. A function $f:X\to[0,\infty]$ (values in the extended half-line of Measure, Measure Space, and Probability Measure) is called measurable if

for every $a\in\mathbb{R}$; for real-valued $f$ this agrees with measurability with respect to the Borel $\sigma$-algebra of the real line by claim 3 of Rational Intervals and Rays Generate the Borel Sigma-Algebra of the Real Line.

The integral of a measurable $f:X\to[0,\infty]$ with respect to $\mu$ is

with the integral of a nonnegative simple function as defined there; the supremum is the least upper bound of the set of values when that set is bounded above, and $\infty$ otherwise. For a nonnegative simple function the two notions of integral agree, since such a function is its own largest simple minorant.