Description: Any n-dimensional countable set is Lebesgue measurable. This is the second statement in Proposition 115G (e) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ctvonmbl.1 | |
|
ctvonmbl.2 | |
||
ctvonmbl.3 | |
||
Assertion | ctvonmbl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ctvonmbl.1 | |
|
2 | ctvonmbl.2 | |
|
3 | ctvonmbl.3 | |
|
4 | iunid | |
|
5 | 1 | vonmea | |
6 | eqid | |
|
7 | 5 6 | dmmeasal | |
8 | 1 | adantr | |
9 | 2 | sselda | |
10 | 8 9 | snvonmbl | |
11 | 7 3 10 | saliuncl | |
12 | 4 11 | eqeltrrid | |