Description: The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). A direct consequence of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 8-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | vonhoi.x | |- ( ph -> X e. Fin ) |
|
| vonhoi.a | |- ( ph -> A : X --> RR ) |
||
| vonhoi.b | |- ( ph -> B : X --> RR ) |
||
| vonhoi.c | |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) |
||
| vonhoi.l | |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) ) |
||
| Assertion | vonhoi | |- ( ph -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vonhoi.x | |- ( ph -> X e. Fin ) |
|
| 2 | vonhoi.a | |- ( ph -> A : X --> RR ) |
|
| 3 | vonhoi.b | |- ( ph -> B : X --> RR ) |
|
| 4 | vonhoi.c | |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) |
|
| 5 | vonhoi.l | |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) ) |
|
| 6 | eqid | |- dom ( voln ` X ) = dom ( voln ` X ) |
|
| 7 | 1 6 2 3 | hoimbl | |- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) e. dom ( voln ` X ) ) |
| 8 | 4 7 | eqeltrid | |- ( ph -> I e. dom ( voln ` X ) ) |
| 9 | 1 8 | mblvon | |- ( ph -> ( ( voln ` X ) ` I ) = ( ( voln* ` X ) ` I ) ) |
| 10 | 1 2 3 4 5 | ovnhoi | |- ( ph -> ( ( voln* ` X ) ` I ) = ( A ( L ` X ) B ) ) |
| 11 | 9 10 | eqtrd | |- ( ph -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) |