changelog and doc

CHANGELOG_UNRELEASED.md

@@ -49,6 +49,39 @@
 - in `lebesgue_integral.v`:
   + lemma `abse_integralP`
 
+- in `classical_sets.v`:
+  + lemma `set_cons1`
+  + lemma `trivIset_bigcup`
+  + definition `maximal_disjoint_subcollection`
+  + lemma `ex_maximal_disjoint_subcollection`
+
+- in `mathcomp_extra.v`:
+  + lemma `leq_ltn_expn`
+
+- in `lebesgue_measure.v`:
+  + lemma `lebesgue_measurable_ball`
+  + lemmas `measurable_closed_ball`, `lebesgue_measurable_closed_ball`
+
+- in `normedtype.v`:
+  + lemmas `ball0`, `ball_itv`, `closed_ball0`, `closed_ball_itv`
+  + definitions `cpoint`, `radius`, `is_ball`
+  + definition `scale_ball`, notation notation ``` *` ```
+  + lemmas `sub_scale_ball`, `scale_ball1`, `sub1_scale_ball`
+  + lemmas `ball_inj`, `radius0`, `cpoint_ball`, `radius_ball_num`,
+    `radius_ball`, `is_ballP`, `is_ball_ball`, `scale_ball0`,
+    `ballE`, `is_ball_closure`, `scale_ballE`, `cpoint_scale_ball`,
+	`radius_scale_ball`
+  + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover`
+  + definition `vitali_collection_partition`
+  + lemmas `vitali_collection_partition_ub_gt0`,
+    `ex_vitali_collection_partition`, `cover_vitali_collection_partition`,
+	`disjoint_vitali_collection_partition`
+  + lemma `separate_closed_ball_countable`
+  + lemmas `vitali_lemma_infinite`, `vitali_lemma_infinite_cover`
+
+- in `topology.v`:
+  + lemmas `closure_eq0`, `separated_open_countable`
+
 ### Changed
 
 - in `hoelder.v`:
@@ -134,6 +167,8 @@
 
 - in `lebesgue_integral.v`:
   + weaken an hypothesis of `integral_ae_eq`
+- in `classical_sets.v`:
+  + `set_nil` generalized to `eqType`
 
 ### Deprecated
 

theories/normedtype.v

@@ -99,9 +99,13 @@ Require Import ereal reals signed topology prodnormedzmodule.
 (*     the Heine-Borel theorem, which states that the compact sets of R^n are *)
 (*     the closed and bounded sets.                                           *)
 (*                                                                            *)
+(*        cpoint A == the center of the set A if it is an open ball           *)
+(*        radius A == the radius of the set A if it is an open ball           *)
+(*                    radius A has type {nonneg R}                            *)
+(*       is_ball A == boolean predicate that holds when A is an open ball     *)
+(*          k *` A == open ball with center cpoint A and radius k * radius A  *)
 (*   vitali_collection_partition B V r n == subset of indices of V such the   *)
-(*                                   the ball B i as a radius between r/2^n+1 *)
-(*                                   and r/2^n                                *)
+(*                    the ball B i as a radius between r/2^n+1 and r/2^n      *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -6311,7 +6315,7 @@ rewrite [in LHS](ballE ballA) (scale_ballE _ _ (ltW k0))// cpoint_ball//.
 by rewrite mulr_gt0.
 Qed.
 
-Lemma radius_sball (A : set R) (k : R) : 0 <= k -> is_ball A ->
+Lemma radius_scale_ball (A : set R) (k : R) : 0 <= k -> is_ball A ->
   (radius (k *` A))%:num = k * (radius A)%:num.
 Proof.
 move=> k0 ballA.
@@ -6608,7 +6612,7 @@ exists j; split => //.
     rewrite (ballE (is_ballB j)) scale_ballE; last by [].
     by rewrite radius_ball_num ?mulr_ge0// mulr_gt0.
   rewrite /closed_ball_ /= cpoint_scale_ball; [|by []..].
-  rewrite radius_sball//.
+  rewrite radius_scale_ball//.
   apply: (@le_trans _ _ (2 * (radius (B i))%:num + (radius (B j))%:num)).
     case: BiBj => y [Biy Bjy].
     rewrite (le_trans (ler_dist_add y _ _))// [in leRHS]addrC ler_add//.