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 | |- voln = ( x e. Fin |-> ( ( voln* ` x ) |` ( CaraGen ` ( voln* ` x ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cvoln | |- voln |
|
| 1 | vx | |- x |
|
| 2 | cfn | |- Fin |
|
| 3 | covoln | |- voln* |
|
| 4 | 1 | cv | |- x |
| 5 | 4 3 | cfv | |- ( voln* ` x ) |
| 6 | ccaragen | |- CaraGen |
|
| 7 | 5 6 | cfv | |- ( CaraGen ` ( voln* ` x ) ) |
| 8 | 5 7 | cres | |- ( ( voln* ` x ) |` ( CaraGen ` ( voln* ` x ) ) ) |
| 9 | 1 2 8 | cmpt | |- ( x e. Fin |-> ( ( voln* ` x ) |` ( CaraGen ` ( voln* ` x ) ) ) ) |
| 10 | 0 9 | wceq | |- voln = ( x e. Fin |-> ( ( voln* ` x ) |` ( CaraGen ` ( voln* ` x ) ) ) ) |