From 99a461bc6f2aa01786e13f599c395299b858c590 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 6 Feb 2023 09:52:01 -0500 Subject: [PATCH] fixing changelog again --- CHANGELOG_UNRELEASED.md | 92 +++-------------------------------------- 1 file changed, 5 insertions(+), 87 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8d97c85a0..30570d33e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`: