Definition df-voln 39429

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

Step	Hyp	Ref	Expression
1		cvoln 39428	. 2 class voln
2		vx	. . 3 setvar 𝑥
3		cfn 7841	. . 3 class Fin
4	2	cv 1474	. . . . 5 class 𝑥
5		covoln 39426	. . . . 5 class voln*
6	4, 5	cfv 5804	. . . 4 class (voln*‘𝑥)
7		ccaragen 39381	. . . . 5 class CaraGen
8	6, 7	cfv 5804	. . . 4 class (CaraGen‘(voln*‘𝑥))
9	6, 8	cres 5040	. . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
10	2, 3, 9	cmpt 4643	. 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
11	1, 10	wceq 1475	1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))

This definition is referenced by:  vonval  39430