nitpicking

CHANGELOG_UNRELEASED.md

@@ -8,14 +8,6 @@
   + `kseries` is now an instance of `Kernel_isSFinite_subdef`
 - in `classical_sets.v`:
   + lemma `setU_id2r`
-- in `topology.v`:
-  + lemma `globally0`
-- in `normedtype.v`:
-  + lemma `lipschitz_set0`, `lipschitz_set1`
-- in `measure.v`:
-  + lemma `measurable_fun_bigcup`
-- in `sequences.v`:
-  + lemma `eq_eseriesl`
 - in `lebesgue_measure.v`:
   + lemma `compact_measurable`
 
@@ -60,54 +52,6 @@
 
 - in `constructive_ereal.v`:
   + lemma `bigmaxe_fin_num`
-  + lemmas `lee_sqr`, `lte_sqr`, `lee_sqrE`, `lte_sqrE`, `sqre_ge0`,
-    `EFin_expe`, `sqreD`, `sqredD`
-- in `probability.v`
-  + definition of `covariance`
-  + lemmas `expectation_sum`, `covarianceE`, `covarianceC`,
-    `covariance_fin_num`, `covariance_cst_l`, `covariance_cst_r`,
-    `covarianceZl`, `covarianceZr`, `covarianceNl`, `covarianceNr`,
-    `covarianceNN`, `covarianceDl`, `covarianceDr`, `covarianceBl`,
-    `covarianceBr`, `variance_fin_num`, `varianceZ`, `varianceN`,
-    `varianceD`, `varianceB`, `varianceD_cst_l`, `varianceD_cst_r`,
-    `varianceB_cst_l`, `varianceB_cst_r`
-- in `functions.v`:
-  + lemma `sumrfctE`
-- in `lebesgue_integral.v`:
-  + lemma `integrable_sum`
-- in `probability.v`
-  + lemma `cantelli`
-- in `classical_sets.v`:
-  + lemmas `preimage_mem_true`, `preimage_mem_false`
-- in `measure.v`:
-  + definition `measure_dominates`, notation `` `<< ``
-  + lemma `measure_dominates_trans`
-- in `measure.v`:
-  + defintion `mfrestr`
-- in `charge.v`:
-  + definition `measure_of_charge`
-  + definition `crestr0`
-  + definitions `jordan_neg`, `jordan_pos`
-  + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates`
-  + lemma `radon_nikodym_finite`
-  + definition `Radon_Nikodym`, notation `'d nu '/d mu`
-  + theorems `Radon_Nikodym_integrable`, `Radon_Nikodym_integral`
-
-- in `measure.v`:
-  + lemmas `measurable_pair1`, `measurable_pair2`
-  + lemma `covariance_le`
-- in `mathcomp_extra.v`
-  + definition `coefE` (will be in MC 2.1/1.18)
-  + lemmas `deg2_poly_canonical`, `deg2_poly_factor`, `deg2_poly_min`,
-    `deg2_poly_minE`, `deg2_poly_ge0`, `Real.deg2_poly_factor`,
-    `deg_le2_poly_delta_ge0`, `deg_le2_poly_ge0`
-    (will be in MC 2.1/1.18)
-  + lemma `deg_le2_ge0`
-  + new lemmas `measurable_subring`, and `semiring_sigma_additive`.
-  + added factory `Content_SubSigmaAdditive_isMeasure`
-
-- in `lebesgue_integral.v`:
-  + lemmas `integrableP`, `measurable_int`
 
 - in file `cantor.v`,
   + new definitions `cantor_space`, `cantor_like`, `pointedDiscrete`, and