proposition: Lemma vitali_lemma_infinite_cover : { D : set I | [/\ countable D, D `<=` V, trivIset D (closure\o B) & cover V (closure\o B) `<=` cover D (closure \o scale_ball 5%:R \o B)] }.
proof: Proof. have [D [cD DV tD maxD]] := vitali_lemma_infinite. exists D; split => // x [i Vi] cBix/=. by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule