Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-voln Structured version   Visualization version   GIF version

Definition df-voln 42822
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
StepHypRef Expression
1 cvoln 42821 . 2 class voln
2 vx . . 3 setvar 𝑥
3 cfn 8508 . . 3 class Fin
42cv 1532 . . . . 5 class 𝑥
5 covoln 42819 . . . . 5 class voln*
64, 5cfv 6354 . . . 4 class (voln*‘𝑥)
7 ccaragen 42774 . . . . 5 class CaraGen
86, 7cfv 6354 . . . 4 class (CaraGen‘(voln*‘𝑥))
96, 8cres 5556 . . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
102, 3, 9cmpt 5145 . 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
111, 10wceq 1533 1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  vonval  42823
  Copyright terms: Public domain W3C validator