vitali lemma (finite) returns uniq

theories/lebesgue_integral.v

@@ -5923,30 +5923,22 @@ have KDB : K `<=` cover [set` D] B.
   by apply: (subset_trans Kcover) => /= x [r Dr] rx; exists r.
 have is_ballB i : is_ball (B i) by exact: is_ball_ball.
 have Bset0 i : B i !=set0 by exists i; exact: ballxx.
-have [E [ED tEB DE]] := @vitali_lemma_finite_cover _ _ B is_ballB Bset0 D.
-pose E' := undup E.
-have {ED}E'D : {subset E' <= D} by move=> x; rewrite mem_undup => /ED.
-have {tEB}tE'B : trivIset [set` E'] B.
-  by apply: sub_trivIset tEB => x/=; rewrite mem_undup.
-have {DE}DE' : cover [set` D] B `<=`
-               cover [set` E'] (scale_ball 3%:R \o B).
-  by move=> x /DE [r/= rE] Brx; exists r => //=; rewrite mem_undup.
-have uniqE' : uniq E' by exact: undup_uniq.
-rewrite (@le_trans _ _ (3%:R%:E * \sum_(i <- E') mu (B i)))//.
-  have {}DE' := subset_trans KDB DE'.
+have [E [uE ED tEB DE]] := @vitali_lemma_finite_cover _ _ B is_ballB Bset0 D.
+rewrite (@le_trans _ _ (3%:R%:E * \sum_(i <- E) mu (B i)))//.
+  have {}DE := subset_trans KDB DE.
   apply: (le_trans (@content_sub_additive _ _ _ [the measure _ _ of mu]
-      K (fun i => 3%:R *` B (nth 0%R E' i)) (size E') _ _ _)) => //.
+      K (fun i => 3%:R *` B (nth 0%R E i)) (size E) _ _ _)) => //.
   - by move=> k ?; rewrite scale_ballE//; exact: measurable_ball.
   - by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff.
-  - apply: (subset_trans DE'); rewrite /cover bigcup_seq.
+  - apply: (subset_trans DE); rewrite /cover bigcup_seq.
     by rewrite (big_nth 0%R)//= big_mkord.
   - rewrite ge0_sume_distrr//= (big_nth 0%R) big_mkord; apply: lee_sum => i _.
     rewrite scale_ballE// !lebesgue_measure_ball ?mulr_ge0 ?(ltW (r_pos _))//.
     by rewrite -mulrnAr EFinM.
 rewrite !EFinM -muleA lee_wpmul2l//=.
 apply: (@le_trans _ _
-    (\sum_(i <- E') c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)).
-  rewrite big_seq [in leRHS]big_seq; apply: lee_sum => r /E'D /Dsub /[!inE] rD.
+    (\sum_(i <- E) c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)).
+  rewrite big_seq [in leRHS]big_seq; apply: lee_sum => r /ED /Dsub /[!inE] rD.
   by rewrite -lee_pdivr_mull ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int.
 rewrite -ge0_sume_distrr//; last by move=> x _; rewrite integral_ge0.
 rewrite lee_wpmul2l//; first by rewrite lee_fin invr_ge0 ltW.

theories/normedtype.v

@@ -6424,7 +6424,7 @@ Hypothesis is_ballB : forall i, is_ball (B i).
 Hypothesis B_set0 : forall i, B i !=set0.
 
 Lemma vitali_lemma_finite (s : seq I) :
-  { D : 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,
@@ -6435,17 +6435,26 @@ 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 [Ds trivIset_DB H]]; exists D; split => //.
+  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 [ujt trivIset_uB H]].
+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].
@@ -6481,11 +6490,11 @@ move=> _ /[1!inE] /predU1P[->|/H//]; exists k; split; [exact: ku| | |].
 Qed.
 
 Lemma vitali_lemma_finite_cover (s : seq I) :
-  { D : seq I | [/\ {subset D <= s},
+  { D : seq I | [/\ uniq D, {subset D <= s},
     trivIset [set` D] B &
     cover [set` s] B `<=` cover [set` D] (scale_ball 3%:R \o B)] }.
 Proof.
-have [D [DV tD maxD]] := vitali_lemma_finite s.
+have [D [uD DV tD maxD]] := vitali_lemma_finite s.
 exists D; split => // x [i Vi] cBix/=.
 by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j.
 Qed.