Definition df-voln 45241

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 45240	. 2 class voln
2		vx	. . 3 setvar 𝑥
3		cfn 8935	. . 3 class Fin
4	2	cv 1540	. . . . 5 class 𝑥
5		covoln 45238	. . . . 5 class voln*
6	4, 5	cfv 6540	. . . 4 class (voln*‘𝑥)
7		ccaragen 45193	. . . . 5 class CaraGen
8	6, 7	cfv 6540	. . . 4 class (CaraGen‘(voln*‘𝑥))
9	6, 8	cres 5677	. . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
10	2, 3, 9	cmpt 5230	. 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
11	1, 10	wceq 1541	1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))

This definition is referenced by:  vonval  45242