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 | ⊢ ( 𝜑 → 𝑋 ∈ Fin ) | |
| Assertion | vonmea | ⊢ ( 𝜑 → ( voln ‘ 𝑋 ) ∈ Meas ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vonmea.1 | ⊢ ( 𝜑 → 𝑋 ∈ Fin ) | |
| 2 | 1 | vonval | ⊢ ( 𝜑 → ( voln ‘ 𝑋 ) = ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ) |
| 3 | 1 | ovnome | ⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas ) |
| 4 | eqid | ⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) | |
| 5 | 3 4 | caratheodory | ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ∈ Meas ) |
| 6 | 2 5 | eqeltrd | ⊢ ( 𝜑 → ( voln ‘ 𝑋 ) ∈ Meas ) |