Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of Fremlin1 p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hoidmv1le.l | |
|
hoidmv1le.z | |
||
hoidmv1le.x | |
||
hoidmv1le.a | |
||
hoidmv1le.b | |
||
hoidmv1le.c | |
||
hoidmv1le.d | |
||
hoidmv1le.s | |
||
Assertion | hoidmv1le | |