Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-voln Structured version   Visualization version   GIF version

Definition df-voln 42698
Description: Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Assertion
Ref Expression
df-voln voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))

Detailed syntax breakdown of Definition df-voln
StepHypRef Expression
1 cvoln 42697 . 2 class voln
2 vx . . 3 setvar 𝑥
3 cfn 8497 . . 3 class Fin
42cv 1527 . . . . 5 class 𝑥
5 covoln 42695 . . . . 5 class voln*
64, 5cfv 6348 . . . 4 class (voln*‘𝑥)
7 ccaragen 42650 . . . . 5 class CaraGen
86, 7cfv 6348 . . . 4 class (CaraGen‘(voln*‘𝑥))
96, 8cres 5550 . . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
102, 3, 9cmpt 5137 . 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
111, 10wceq 1528 1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  vonval  42699
  Copyright terms: Public domain W3C validator