proposition: Lemma vitali_lemma_finite (s : seq I) : { D : seq I | [/\ uniq D, {subset D <= s}, trivIset [set` D] B & forall i, i \in s -> exists j, [/\ j \in D, B i `&` B j !=set0, radius (B j) >= radius (B i) & B i `<=` 3%:R *` B j] ] }.
proof: Proof. pose LE x y := radius (B x) <= radius (B y). have LE_trans : transitive LE by move=> x y z; exact: le_trans. wlog : s / sorted LE s. have : sorted LE (sort LE s) by apply: sort_sorted => x y; exact: le_total. move=> /[swap] /[apply] -[D [uD Ds trivIset_DB H]]; exists D; split => //. - by move=> x /Ds; rewrite mem_sort. - by move=> i; rewrite -(mem_sort LE) => /H. elim: s => [_|i [/= _ _|j t]]; first by exists nil. exists [:: i]; split => //; first by rewrite set_cons1; exact: trivIset1. move=> _ /[1!inE] /eqP ->; exists i; split => //; first by rewrite mem_head. - by rewrite setIid; exact: B_set0. - exact: sub1_scale_ball. rewrite /= => + /andP[ij jt] => /(_ jt)[u [uu ujt trivIset_uB H]]. have [K|] := pselect (forall j, j \in u -> B j `&` B i = set0). have [iu|iu] := boolP (i \in u). exists u; split => //. - by move=> x /ujt xjt; rewrite inE xjt orbT. - move=> k /[1!inE] /predU1P[->{k}|]. exists i; split; [by []| |exact: lexx|]. by rewrite setIid; exact: B_set0. exact: sub1_scale_ball. by move/H => [l [lu lk0 kl k3l]]; exists l; split => //; rewrite inE lu orbT. exists (i :: u); split => //. - by rewrite /= iu. - move=> x /[1!inE] /predU1P[->|]; first by rewrite mem_head. by move/ujt => xjt; rewrite in_cons xjt orbT. - move=> k l /= /[1!inE] /predU1P[->{k}|ku]. by move=> /predU1P[->{j}//|js] /set0P; rewrite setIC K// eqxx. by move=> /predU1P[->{l} /set0P|lu]; [rewrite K// eqxx|exact: trivIset_uB]. - move=> k /[1!inE] /predU1P[->{k}|]. exists i; split; [by rewrite mem_head| |exact: lexx|]. by rewrite setIid; exact: B_set0. exact: sub1_scale_ball. by move/H => [l [lu lk0 kl k3l]]; exists l; split => //; rewrite inE lu orbT. move/existsNP/cid => [k /not_implyP[ku /eqP/set0P ki0]]. exists u; split => //. by move=> l /ujt /[!inE] /predU1P[->|->]; rewrite ?eqxx ?orbT. move=> _ /[1!inE] /predU1P[->|/H//]; exists k; split; [exact: ku| | |]. - by rewrite setIC. - apply: (le_trans ij); move/ujt : ku => /[1!inE] /predU1P[<-|kt]. exact: lexx. by have /allP := order_path_min LE_trans jt; apply; exact: kt. - case: ki0 => x [Bkx Bix] y => iy. rewrite (ballE (is_ballB k)) scale_ballE// /ball/=. rewrite -(subrK x y) -(addrC x) opprD addrA opprB. rewrite (le_lt_trans (ler_normD _ _))// -nat1r mulrDl mul1r mulr_natl. rewrite (ltrD (is_ballP (is_ballB k) _))// -(subrK (cpoint (B i)) y). rewrite -(addrC (cpoint (B i))) opprD addrA opprB. rewrite (le_lt_trans (ler_normD _ _))//. apply (@lt_le_trans _ _ ((radius (B j))%:num *+ 2)); last first. apply: ler_wMn2r; move/ujt : ku; rewrite inE => /predU1P[<-|kt]. exact: lexx. by have /allP := order_path_min LE_trans jt; apply; exact: kt. rewrite mulr2n ltrD//. by rewrite distrC (lt_le_trans (is_ballP (is_ballB i) _)). by rewrite (lt_le_trans (is_ballP (is_ballB i) _)). 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