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 40516
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 40515 . 2 class voln
2 vx . . 3 setvar 𝑥
3 cfn 7940 . . 3 class Fin
42cv 1480 . . . . 5 class 𝑥
5 covoln 40513 . . . . 5 class voln*
64, 5cfv 5876 . . . 4 class (voln*‘𝑥)
7 ccaragen 40468 . . . . 5 class CaraGen
86, 7cfv 5876 . . . 4 class (CaraGen‘(voln*‘𝑥))
96, 8cres 5106 . . 3 class ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))
102, 3, 9cmpt 4720 . 2 class (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
111, 10wceq 1481 1 wff voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  vonval  40517
  Copyright terms: Public domain W3C validator