Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of Fremlin1 p. 29, case nonempty interval and dimension of the space greater than 1 . (Contributed by Glauco Siliprandi, 21-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hoidmvlelem4.l | |
|
hoidmvlelem4.x | |
||
hoidmvlelem4.y | |
||
hoidmvlelem4.n | |
||
hoidmvlelem4.z | |
||
hoidmvlelem4.w | |
||
hoidmvlelem4.a | |
||
hoidmvlelem4.b | |
||
hoidmvlelem4.k | |
||
hoidmvlelem4.c | |
||
hoidmvlelem4.d | |
||
hoidmvlelem4.r | |
||
hoidmvlelem4.h | |
||
hoidmvlelem4.14 | |
||
hoidmvlelem4.e | |
||
hoidmvlelem4.u | |
||
hoidmvlelem4.s | |
||
hoidmvlelem4.i | |
||
hoidmvlelem4.i2 | |
||
Assertion | hoidmvlelem4 | |