Definition df-voln 46568

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 46567	. 2 class voln
2		vx	. . 3 setvar 𝑥
3		cfn 8959	. . 3 class Fin
4	2	cv 1539	. . . . 5 class 𝑥
5		covoln 46565	. . . . 5 class voln*
6	4, 5	cfv 6531	. . . 4 class (voln*‘𝑥)
7		ccaragen 46520	. . . . 5 class CaraGen
8	6, 7	cfv 6531	. . . 4 class (CaraGen‘(voln*‘𝑥))
9	6, 8	cres 5656	. . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
10	2, 3, 9	cmpt 5201	. 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
11	1, 10	wceq 1540	1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))

This definition is referenced by:  vonval  46569