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 43603
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 43602 . 2 class voln
2 vx . . 3 setvar 𝑥
3 cfn 8548 . . 3 class Fin
42cv 1541 . . . . 5 class 𝑥
5 covoln 43600 . . . . 5 class voln*
64, 5cfv 6333 . . . 4 class (voln*‘𝑥)
7 ccaragen 43555 . . . . 5 class CaraGen
86, 7cfv 6333 . . . 4 class (CaraGen‘(voln*‘𝑥))
96, 8cres 5521 . . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
102, 3, 9cmpt 5107 . 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
111, 10wceq 1542 1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  vonval  43604
  Copyright terms: Public domain W3C validator