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 | 0fi | |- (/) 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 ) |