Lemma 1

Tag 096Y, permanent. Cite it as [Bourbaki, Tag 096Y].

For every numerical function $f \geqslant 0$ defined on X,

\int^* f_t \, d\mu' = \int^* f \, d\lambda'_t.

Since $t' \mapsto (t, t')$ is a continuous and proper mapping, this follows from Prop. 2 of §4, No. 2.

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.

Cited by