cleaning

- move lemmas to more appropriate locations
- changelog

CHANGELOG_UNRELEASED.md

@@ -169,6 +169,20 @@
     `measurable_closed_ball`, `lebesgue_measure_closed_ball`,
     `measurable_scale_cball`
 
+- in `classical_sets.v`:
+  + lemmas `trivIsetT_bigcup`, `mem_not_I`
+
+- in `sequences.v`:
+  + lemma `nneseries_tail_cvg`
+
+- in `normedtype.v`:
+  + lemmas `open_subball`, `closed_disjoint_closed_ball`
+
+- in `lebesgue_measure.v`:
+  + lemmas `measure_sigma_sub_additive_tail`, `outer_measure_sigma_subadditive_tail`
+  + definition `vitali_cover`
+  + lemma `vitali_theorem`
+
 ### Changed
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized

classical/classical_sets.v

@@ -1124,6 +1124,9 @@ Proof. by move=> k; apply/val_inj. Qed.
 Lemma IIordK {n} : cancel (@IIord n) ordII.
 Proof. by move=> k; apply/val_inj. Qed.
 
+Lemma mem_not_I N n : (n \in ~` `I_N) = (N <= n).
+Proof. by rewrite in_setC /mkset /in_mem /mem /= /in_set asboolb -leqNgt. Qed.
+
 End InitialSegment.
 
 Lemma setT_unit : [set: unit] = [set tt].
@@ -2567,6 +2570,17 @@ have [nm|nm] := eqVneq n m; first by apply: (tB m) => //; rewrite -nm.
 exact: (H _ _ _ _ nm).
 Qed.
 
+Lemma trivIsetT_bigcup T1 T2 (I : eqType) (D : I -> set T1) (F : T1 -> set T2) :
+  trivIset setT D ->
+  trivIset (\bigcup_i D i) F ->
+  trivIset setT (fun i => \bigcup_(t in D i) F t).
+Proof.
+move=> D0 h i j _ _ [t [[m Dim Fmt] [n Djn Fnt]]].
+have mn : m = n by apply: h => //; [exists i|exists j|exists t].
+rewrite {}mn {m} in Dim Fmt *.
+by apply: D0 => //; exists n.
+Qed.
+
 Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i.
 
 Lemma coverE T I D (F : I -> set T) : cover D F = \bigcup_(i in D) F i.