Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. This proof handles the non-trivial cases (nonzero dimension and finite outer measure). (Contributed by Glauco Siliprandi, 24-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hspmbllem3.h | |
|
hspmbllem3.x | |
||
hspmbllem3.i | |
||
hspmbllem3.y | |
||
hspmbllem3.a | |
||
hspmbllem3.s | |
||
hspmbllem3.c | |
||
hspmbllem3.l | |
||
hspmbllem3.d | |
||
hspmbllem3.10 | |
||
hspmbllem3.11 | |
||
Assertion | hspmbllem3 | |