# Metamath Proof Explorer

## Definition df-voln

Description: Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of x is the dimension of the space modeled. Definition 115C of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion df-voln ${⊢}\mathrm{voln}=\left({x}\in \mathrm{Fin}⟼{\mathrm{voln*}\left({x}\right)↾}_{\mathrm{CaraGen}\left(\mathrm{voln*}\left({x}\right)\right)}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cvoln ${class}\mathrm{voln}$
1 vx ${setvar}{x}$
2 cfn ${class}\mathrm{Fin}$
3 covoln ${class}\mathrm{voln*}$
4 1 cv ${setvar}{x}$
5 4 3 cfv ${class}\mathrm{voln*}\left({x}\right)$
6 ccaragen ${class}\mathrm{CaraGen}$
7 5 6 cfv ${class}\mathrm{CaraGen}\left(\mathrm{voln*}\left({x}\right)\right)$
8 5 7 cres ${class}\left({\mathrm{voln*}\left({x}\right)↾}_{\mathrm{CaraGen}\left(\mathrm{voln*}\left({x}\right)\right)}\right)$
9 1 2 8 cmpt ${class}\left({x}\in \mathrm{Fin}⟼{\mathrm{voln*}\left({x}\right)↾}_{\mathrm{CaraGen}\left(\mathrm{voln*}\left({x}\right)\right)}\right)$
10 0 9 wceq ${wff}\mathrm{voln}=\left({x}\in \mathrm{Fin}⟼{\mathrm{voln*}\left({x}\right)↾}_{\mathrm{CaraGen}\left(\mathrm{voln*}\left({x}\right)\right)}\right)$