Description: The Lebesgue measure (for the zero dimensional space of reals) of every measurable set is zero. (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | von0val.1 | |- ( ph -> A e. dom ( voln ` (/) ) ) |
|
Assertion | von0val | |- ( ph -> ( ( voln ` (/) ) ` A ) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | von0val.1 | |- ( ph -> A e. dom ( voln ` (/) ) ) |
|
2 | 0fin | |- (/) e. Fin |
|
3 | 2 | a1i | |- ( ph -> (/) e. Fin ) |
4 | 3 1 | mblvon | |- ( ph -> ( ( voln ` (/) ) ` A ) = ( ( voln* ` (/) ) ` A ) ) |
5 | 3 1 | vonmblss2 | |- ( ph -> A C_ ( RR ^m (/) ) ) |
6 | 5 | ovn0val | |- ( ph -> ( ( voln* ` (/) ) ` A ) = 0 ) |
7 | 4 6 | eqtrd | |- ( ph -> ( ( voln ` (/) ) ` A ) = 0 ) |