Mini-Vitali covering theorem

Work with the covering relation $\mathcal{H} = \{ ([u,v], w) : u < v, \ u \le w \le v \}$ and the premeasure $\ell([u,v], w) = v - u$. A family $\beta \subseteq \mathcal{H}$ is a full cover of $E$ when for each $x \in E$ there is $\delta > 0$ with $([u,v], x) \in \beta$ whenever $u \le x \le v$ and $v - u < \delta$, and a fine cover of $E$ when for each $x \in E$ and each $\delta > 0$ some $([u,v], x) \in \beta$ has $v - u < \delta$. Write $V(\ell, \beta)$ for the supremum of $\sum_i (v_i - u_i)$ over packings, that is over finite or countable subfamilies of $\beta$ with pairwise nonoverlapping intervals.

Mini-Vitali covering theorem. For $E \subseteq \mathbb{R}$ the following are equivalent, and each says that $E$ has Lebesgue measure zero:

1. for every $\varepsilon > 0$ there is an open $G \supseteq E$ with $\lambda(G) < \varepsilon$;
2. for every $\varepsilon > 0$ there is a full cover $\beta$ of $E$ with $V(\ell, \beta) < \varepsilon$;
3. for every $\varepsilon > 0$ there is a fine cover $\beta$ of $E$ with $V(\ell, \beta) < \varepsilon$.

Not proved in this library. It is recorded with citations and used in no proof here.

What would prove it. Two elementary covering lemmas about finite families of compact intervals, then a compactness argument; Bruckner, Bruckner and Thomson give it in Section 3.10 as the cheap precursor to the full theorem. It is genuinely easier than Vitali covering theorem ‡, because it is the same assertion restricted to null sets: the full theorem says $\ell^{\circ} = \ell^{\bullet} = \lambda^{*}$ for the measures generated by covers and by packings, and the mini version says only that the three vanish together.

Which page it serves. The same pages as the full theorem, and it is the piece that a first pass at a measure track should prove first: it already yields the Lebesgue differentiation theorem for monotone functions (Lebesgue's differentiation theorem for monotone functions ‡) by the growth lemma route, without the full covering theorem.

Why it is deferred at all, given that the elementary null sets are in scope. The statement is about Lebesgue measure zero, which this library does have in the elementary covering sense, but its content is the equivalence with the full and fine cover formulations, and those are the language of the measure track. Nothing on the topology of $\mathbb{R}$ page or the Riemann integral page currently needs them, so there is no loss; a future measure page will state and prove this before anything else.