Description: ( volnX ) is a measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set X . Comments in Definition 115E of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | vonmea.1 | |- ( ph -> X e. Fin ) |
|
| Assertion | vonmea | |- ( ph -> ( voln ` X ) e. Meas ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vonmea.1 | |- ( ph -> X e. Fin ) |
|
| 2 | 1 | vonval | |- ( ph -> ( voln ` X ) = ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) ) |
| 3 | 1 | ovnome | |- ( ph -> ( voln* ` X ) e. OutMeas ) |
| 4 | eqid | |- ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) ) |
|
| 5 | 3 4 | caratheodory | |- ( ph -> ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) e. Meas ) |
| 6 | 2 5 | eqeltrd | |- ( ph -> ( voln ` X ) e. Meas ) |