Corollary 2

— Let $\mathbf{H}$ be a nonempty set, directed for the relation $\leqslant$ (resp. $\geqslant$), of lower (resp. upper) semi-continuous and integrable numerical functions; if

then the upper (resp. lower) envelope $g$ of $\mathbf{H}$ is integrable,

and $\int g \, d|\mu| = \sup_{f \in \mathbf{H}} \int f \, d|\mu|$ (resp. $\int g \, d|\mu| = \inf_{f \in \mathbf{H}} \int f \, d|\mu|$).

We may limit ourselves to the case of lower semi-continuous functions; the functions $f^+$ (resp. $f^-$), as $f$ runs over $\mathbf{H}$, then form a directed set for $\leqslant$ (resp. $\geqslant$) of lower (resp. upper) semi-continuous functions $\geqslant 0$; the upper (resp. lower) envelope of the $f^+$ (resp. $f^-$), for $f \in \mathbf{H}$, is equal to $g^+$ (resp. $g^-$). On the other hand, one can replace $\mathbf{H}$ by one of its sections (which is cofinal to it), consisting of the $f \in \mathbf{H}$ that are $\geqslant f_0$, for some function $f_0 \in \mathbf{H}$; then $\int f^+ \, d|\mu| \leqslant \int f \, d|\mu| + \int f_0^- \, d|\mu|$; we thus see that we are reduced to proving the two assertions of the corollary when $\mathbf{H}$ consists of positive functions. If $\mathbf{H}$ is directed for $\leqslant$ and consists of lower semi-continuous functions $\geqslant 0$, then we know (§ 1, No. 1, Th. 1) that

therefore $g$, which is lower semi-continuous, is integrable by Prop. 5; we have $\int g \, d|\mu| = \lim_{f \in \mathbf{H}} \int f \, d|\mu|$ and, since $f \leqslant g$, $\lim_{f \in \mathbf{H}} N_1(g - f) = 0$, which shows that $f$ converges in mean to $g$ with respect to $\mathbf{H}$, and thus proves the corollary in this case. If $\mathbf{H}$ is directed for $\geqslant$ and consists of upper semi-continuous integrable functions $f$ such that $0 \leqslant f \leqslant f_1$ with $f_1 \in \mathbf{H}$, then there exists a lower semi-continuous integrable function $h$ such that $f_1 \leqslant h$; we may write $f = h - f'$, where $f'(x) = h(x) - f(x)$ when $f(x) < +\infty$, and $f'(x) = 0$ otherwise. It is clear that the $f'$ form a directed set, for $\leqslant$, of lower semi-continuous integrable functions $\geqslant 0$, with

we can apply to them what has been proved above; if $g'$ is the upper envelope of the $f'$, then $h$ and $g'$ are finite almost everywhere, therefore $h - g'$ is defined almost everywhere and is equal to $g$ almost everywhere; from this, the conclusions of the corollary follow at once in this case.