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 39229
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 39228 . 2 class voln
2 vx . . 3 setvar 𝑥
3 cfn 7814 . . 3 class Fin
42cv 1473 . . . . 5 class 𝑥
5 covoln 39226 . . . . 5 class voln*
64, 5cfv 5786 . . . 4 class (voln*‘𝑥)
7 ccaragen 39181 . . . . 5 class CaraGen
86, 7cfv 5786 . . . 4 class (CaraGen‘(voln*‘𝑥))
96, 8cres 5026 . . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
102, 3, 9cmpt 4633 . 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
111, 10wceq 1474 1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  vonval  39230
  Copyright terms: Public domain W3C validator