Definition df-voln 44077

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 44076	. 2 class voln
2		vx	. . 3 setvar 𝑥
3		cfn 8733	. . 3 class Fin
4	2	cv 1538	. . . . 5 class 𝑥
5		covoln 44074	. . . . 5 class voln*
6	4, 5	cfv 6433	. . . 4 class (voln*‘𝑥)
7		ccaragen 44029	. . . . 5 class CaraGen
8	6, 7	cfv 6433	. . . 4 class (CaraGen‘(voln*‘𝑥))
9	6, 8	cres 5591	. . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
10	2, 3, 9	cmpt 5157	. 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
11	1, 10	wceq 1539	1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))

This definition is referenced by:  vonval  44078