fixing changelog again

CHANGELOG_UNRELEASED.md

@@ -43,93 +43,6 @@
   + lemmas `integral0_eq`, `fubini_tonelli`
   + product measures now take `{measure _ -> _}` arguments and their
     theory quantifies over a `{sigma_finite_measure _ -> _}`.
-  + definition `ErealGenInftyO.R` and lemma `ErealGenInftyO.measurableE`
-  + lemma `sub1set`
-- in `constructive_ereal.v`:
-  + lemmas `lteN10`, `leeN10`
-  + lemmas `le0_fin_numE`
-  + lemmas `fine_lt0`, `fine_le0`
-- in `sequences.v`:
-  + lemmas `is_cvg_ereal_npos_natsum_cond`, `lee_npeseries`,
-    `is_cvg_npeseries_cond`, `is_cvg_npeseries`, `npeseries_le0`,
-    `is_cvg_ereal_npos_natsum`
-  + lemma `nnseries_is_cvg`
-- in `constructive_ereal.v`:
-  + lemma `fine_lt0E`
-- in file `normedtype.v`
-  + lemmas `closed_ballR_compact` and `locally_compactR`
-
-- in `sequences.v`:
-  + lemma `invr_cvg0` and `invr_cvg_pinfty`
-  + lemma `cvgPninfty_lt`, `cvgPpinfty_near`, `cvgPninfty_near`,
-    `cvgPpinfty_lt_near` and `cvgPninfty_lt_near`
-- in `classical_sets.v`:
-  + notations `\bigcup_(i < n) F` and `\bigcap_(i < n) F`
-
-- in `fsbig.v`:
-  + lemma `fsbig_setU_set1`
-- in `tooplogy.v`:
-  + lemmas `closed_bigsetU`, `accessible_finite_set_closed`
-
-
-- in file `classical_sets.v`,
-  + new lemmas `eq_image_id`, `subKimage`, `subimageK`, and `eq_imageK`.
-- in file `functions.v`,
-  + new lemmas `inv_oppr`, `preimageEoinv`, `preimageEinv`, and
-    `inv_funK`.
-- in file `mathcomp_extra.v`,
-  + new definition `inv_fun`.
-  + new lemmas `ler_ltP`, and `real_ltr_distlC`.
-- in file `constructive_ereal.v`,
-  + new lemmas `real_ltey`, `real_ltNye`, `real_leey`, `real_leNye`,
-    `fin_real`, `addNye`, `addeNy`, `gt0_muley`, `lt0_muley`, `gt0_muleNy`, and
-    `lt0_muleNy`.
-  + new lemmas `daddNye`, and `daddeNy`.
-- in file `ereal.v`,
-  + new lemmas `ereal_nbhs_pinfty_gt`, `ereal_nbhs_ninfty_lt`,
-    `ereal_nbhs_pinfty_real`, and `ereal_nbhs_ninfty_real`.
-- in file `normedtype.v`,
-  + new lemmas `nbhsNimage`, `nbhs_pinfty_real`, `nbhs_ninfty_real`,
-    `pinfty_ex_ge`, `cvgryPger`, `cvgryPgtr`, `cvgrNyPler`, `cvgrNyPltr`,
-    `cvgry_ger`, `cvgry_gtr`, `cvgrNy_ler`, `cvgrNy_ltr`, `cvgNry`, `cvgNrNy`,
-    `cvgry_ge`, `cvgry_gt`, `cvgrNy_le`, `cvgrNy_lt`, `cvgeyPger`, `cvgeyPgtr`,
-    `cvgeyPgty`, `cvgeyPgey`, `cvgeNyPler`, `cvgeNyPltr`, `cvgeNyPltNy`,
-    `cvgeNyPleNy`, `cvgey_ger`, `cvgey_gtr`, `cvgeNy_ler`, `cvgeNy_ltr`,
-    `cvgNey`, `cvgNeNy`, `cvgerNyP`, `cvgeyPge`, `cvgeyPgt`, `cvgeNyPle`,
-    `cvgeNyPlt`, `cvgey_ge`, `cvgey_gt`, `cvgeNy_le`, `cvgeNy_lt`, `cvgenyP`,
-    `normfZV`, `fcvgrPdist_lt`, `cvgrPdist_lt`, `cvgrPdistC_lt`,
-    `cvgr_dist_lt`, `cvgr_distC_lt`, `cvgr_dist_le`, `cvgr_distC_le`,
-    `nbhs_norm0P`, `cvgr0Pnorm_lt`, `cvgr0_norm_lt`, `cvgr0_norm_le`, `nbhsDl`,
-    `nbhsDr`, `nbhs0P`, `nbhs_right0P`, `nbhs_left0P`, `nbhs_right_gt`,
-    `nbhs_left_lt`, `nbhs_right_neq`, `nbhs_left_neq`, `nbhs_right_ge`,
-    `nbhs_left_le`, `nbhs_right_lt`, `nbhs_right_le`, `nbhs_left_gt`,
-    `nbhs_left_ge`, `nbhsr0P`, `cvgrPdist_le`, `cvgrPdist_ltp`,
-    `cvgrPdist_lep`, `cvgrPdistC_le`, `cvgrPdistC_ltp`, `cvgrPdistC_lep`,
-    `cvgr0Pnorm_le`, `cvgr0Pnorm_ltp`, `cvgr0Pnorm_lep`, `cvgr_norm_lt`,
-    `cvgr_norm_le`, `cvgr_norm_gt`, `cvgr_norm_ge`, `cvgr_neq0`,
-    `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_gt`, `real_cvgr_ge`, `cvgr_lt`,
-    `cvgr_gt`, `cvgr_norm_lty`, `cvgr_norm_ley`, `cvgr_norm_gtNy`,
-    `cvgr_norm_geNy`, `fcvgr_dist_lt2P`, `cvgr_dist_lt2P`, `cvgr_dist_lt2`,
-    `cvgNP`, `norm_cvg0P`, `cvgVP`, `is_cvgVE`, `cvgr_to_ge`, `cvgr_to_le`,
-    `nbhs_EFin`, `nbhs_ereal_pinfty`, `nbhs_ereal_ninfty`, `fine_fcvg`,
-    `fcvg_is_fine`, `fine_cvg`, `cvg_is_fine`, `cvg_EFin`, `neq0_fine_cvgP`,
-    `cvgeNP`, `is_cvgeNE`, `cvge_to_ge`, `cvge_to_le`, `is_cvgeM`, `limeM`,
-    `cvge_ge`, `cvge_le`, `lim_nnesum`, `ltr0_cvgV0`, `cvgrVNy`, `ler_cvg_to`,
-    `gee_cvgy`, `lee_cvgNy`, `squeeze_fin`, and `lee_cvg_to`.
-- in file `sequences.v`,
-  + new lemma `nneseries_pinfty`.
-- in file `topology.v`,
-  + new lemmas `eq_cvg`, `eq_is_cvg`, `eq_near`, `cvg_toP`, `cvgNpoint`,
-    `filter_imply`, `nbhs_filter`, `near_fun`, `cvgnyPgt`, `cvgnyPgty`,
-    `cvgnyPgey`, `fcvg_ballP`, `fcvg_ball`, and `fcvg_ball2P`.
-- in `topology.v`, added `near do` and `near=> x do` tactic notations
-  to perform some tactics under a `\forall x \near F, ...` quantification.
-- in `normedtype.v`, added notations `^'+`, `^'-`, `+oo_R`, `-oo_R`
-- in `topology.v`
-  + definition `quotient_topology`
-  + definition `quotient_topologicalType_mixin`, `quotient_topologicalType`
-  + definition `quotient_open`
-  + lemma `pi_continuous`, `quotient_continuous`,`repr_comp_continuous`
 
 - in `classical_sets.v`:
   + lemma `trivIset_mkcond`
@@ -151,6 +64,11 @@
   + lemmas `adde_def_doppeD`, `adde_def_doppeB`
   + lemma `fin_num_sume_distrr`
 
+- in file `topology.v`,
+  + new definitions `quotient_topology`, and `quotient_open`.
+  + new lemmas `pi_continuous`, `quotient_continuous`, and
+    `repr_comp_continuous`.
+
 ### Changed
 
 - in `fsbigop.v`: