Definition df-voln 46554

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 46553	. 2 class voln
2		vx	. . 3 setvar 𝑥
3		cfn 8985	. . 3 class Fin
4	2	cv 1539	. . . . 5 class 𝑥
5		covoln 46551	. . . . 5 class voln*
6	4, 5	cfv 6561	. . . 4 class (voln*‘𝑥)
7		ccaragen 46506	. . . . 5 class CaraGen
8	6, 7	cfv 6561	. . . 4 class (CaraGen‘(voln*‘𝑥))
9	6, 8	cres 5687	. . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
10	2, 3, 9	cmpt 5225	. 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
11	1, 10	wceq 1540	1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))

This definition is referenced by:  vonval  46555