Description: The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hsphoidmvle.l | |
|
hsphoidmvle.x | |
||
hsphoidmvle.z | |
||
hsphoidmvle.y | |
||
hsphoidmvle.c | |
||
hsphoidmvle.h | |
||
hsphoidmvle.a | |
||
hsphoidmvle.b | |
||
Assertion | hsphoidmvle | |