Definition df-voln 40753

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.)

Assertion

Ref	Expression
df-voln	|- voln = ( x e. Fin |-> ( (voln* ` x ) |` (CaraGen ` (voln* ` x ) ) ) )

Detailed syntax breakdown of Definition df-voln

Step	Hyp	Ref	Expression
1		cvoln 40752	. 2 class voln
2		vx	. . 3 setvar x
3		cfn 7955	. . 3 class Fin
4	2	cv 1482	. . . . 5 class x
5		covoln 40750	. . . . 5 class voln*
6	4, 5	cfv 5888	. . . 4 class (voln* ` x )
7		ccaragen 40705	. . . . 5 class CaraGen
8	6, 7	cfv 5888	. . . 4 class (CaraGen ` (voln* ` x ) )
9	6, 8	cres 5116	. . 3 class ( (voln* ` x ) |` (CaraGen ` (voln* ` x ) ) )
10	2, 3, 9	cmpt 4729	. 2 class ( x e. Fin |-> ( (voln* ` x ) |` (CaraGen ` (voln* ` x ) ) ) )
11	1, 10	wceq 1483	1 wff voln = ( x e. Fin |-> ( (voln* ` x ) |` (CaraGen ` (voln* ` x ) ) ) )

This definition is referenced by:  vonval  40754