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 = ( 𝑥 ∈ Fin ↦ ( ( voln* ‘ 𝑥 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cvoln | ⊢ voln | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | cfn | ⊢ Fin | |
| 3 | covoln | ⊢ voln* | |
| 4 | 1 | cv | ⊢ 𝑥 |
| 5 | 4 3 | cfv | ⊢ ( voln* ‘ 𝑥 ) |
| 6 | ccaragen | ⊢ CaraGen | |
| 7 | 5 6 | cfv | ⊢ ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) |
| 8 | 5 7 | cres | ⊢ ( ( voln* ‘ 𝑥 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) ) |
| 9 | 1 2 8 | cmpt | ⊢ ( 𝑥 ∈ Fin ↦ ( ( voln* ‘ 𝑥 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) ) ) |
| 10 | 0 9 | wceq | ⊢ voln = ( 𝑥 ∈ Fin ↦ ( ( voln* ‘ 𝑥 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑥 ) ) ) ) |