Merge pull request #278 from math-comp/changelog033

release of version 0.3.3
math-comp · Nov 11, 2020 · ce941d5 · ce941d5
2 parents 8148881 + 7a688d4
commit ce941d5
Show file tree

Hide file tree

Showing 4 changed files with 133 additions and 125 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,136 @@
 # Changelog
 
-Last releases: [[0.3.2] - 2020-08-11](#032---2020-08-11) and [[0.3.1] - 2020-06-11](#031---2020-06-11)
+Last releases: [[0.3.3] - 2020-11-11](#033---2020-11-11) and [[0.3.2] - 2020-08-11](#032---2020-08-11)
+
+## [0.3.3] - 2020-11-11
+
+### Added
+
+- in `boolp.v`:
+  + lemma `not_andP`
+  + lemma `not_exists2P`
+- in `classical_sets.v`:
+  + lemmas `setIIl`, `setIIr`, `setCS`, `setSD`, `setDS`, `setDSS`, `setCI`,
+    `setDUr`, `setDUl`, `setIDA`, `setDD`
+  + definition `dep_arrow_choiceType`
+  + lemma `bigcup_set0`
+  + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `subsetPset`, `properPset`
+  + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType`
+  + lemmas `set0M`, `setM0`, `image_set0_set0`, `subset_set1`, `preimage_set0`
+  + lemmas `setICr`, `setUidPl`, `subsets_disjoint`, `disjoints_subset`, `setDidPl`,
+    `setIidPl`, `setIS`, `setSI`, `setISS`, `bigcup_recl`, `bigcup_distrr`,
+    `setMT`
+  + new lemmas: `lb_set1`, `ub_lb_set1`, `ub_lb_refl`, `lb_ub_lb`
+  + new definitions and lemmas: `infimums`, `infimum`, `infimums_set1`, `is_subset1_infimum`
+  + new lemmas: `ge_supremum_Nmem`, `le_infimum_Nmem`, `nat_supremums_neq0`
+  + lemmas `setUCl`, `setDv`
+  + lemmas `image_preimage_subset`, `image_subset`, `preimage_subset`
+  + definition `proper` and its notation `<`
+  + lemmas `setUK`, `setKU`, `setIK`, `setKI`
+  + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `properEneq`
+  + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` on classical `set`.
+- file `nngnum.v`
+- in `topology.v`:
+  + definition `meets` and its notation `#`
+  + lemmas `meetsC`, `meets_openr`, `meets_openl`, `meets_globallyl`,
+    `meets_globallyr `, `meetsxx` and `proper_meetsxx`.
+  + definition `limit_point`
+  + lemmas `subset_limit_point`, `closure_limit_point`,
+    `closure_subset`, `closureE`, `closureC`, `closure_id`
+  + lemmas `cluster_nbhs`, `clusterEonbhs`, `closureEcluster`
+  + definition `separated`
+  + lemmas `connected0`, `connectedPn`, `connected_continuous_connected`
+  + lemmas `closureEnbhs`, `closureEonbhs`, `limit_pointEnbhs`,
+    `limit_pointEonbhs`, `closeEnbhs`, `closeEonbhs`.
+- in `ereal.v`:
+  + notation `\+` (`ereal_scope`) for function addition
+  + notations `>` and `>=` for comparison of extended real numbers
+  + definition `is_real`, lemmas `is_realN`, `is_realD`, `ERFin_real_of_er`
+  + basic lemmas: `addooe`, `adde_Neq_pinfty`, `adde_Neq_ninfty`, `addERFin`,
+    `subERFin`, `real_of_erN`, `lb_ereal_inf_adherent`
+  + arithmetic lemmas: `oppeD`, `subre_ge0`, `suber_ge0`, `lee_add2lE`, `lte_add2lE`,
+    `lte_add`, `lte_addl`, `lte_le_add`, `lte_subl_addl`, `lee_subr_addr`,
+    `lee_subl_addr`, `lte_spaddr`
+  + lemmas `gee0P`, `sume_ge0`, `lee_sum_nneg`, `lee_sum_nneg_ord`, `lee_sum_nneg_subset`, `lee_sum_nneg_subfset`
+  + lemma `lee_addr`
+  + lemma `lee_adde`
+  + lemma `oppe_continuous`
+  + lemmas `ereal_nbhs_pinfty_ge`, `ereal_nbhs_ninfty_le`
+- in `sequences.v`:
+  + definitions `arithmetic`, `geometric`, `geometric_invn`
+  + lemmas `increasing_series`, `cvg_shiftS`, `mulrn_arithmetic`,
+    `exprn_geometric`, `cvg_arithmetic`, `cvg_expr`,
+    `geometric_seriesE`, `cvg_geometric_series`,
+    `is_cvg_geometric_series`.
+  + lemmas `ereal_cvgN`, `ereal_cvg_ge0`, `ereal_lim_ge`, `ereal_lim_le`
+  + lemma `ereal_cvg_real`
+  + lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series`, `ereal_nneg_series_lim_ge0`,
+    `ereal_nneg_series_pinfty`
+  + lemmas `ereal_cvgPpinfty`, `ereal_cvgPninfty`, `lee_lim`
+  + lemma `ereal_cvgD`
+    * with intermediate lemmas `ereal_cvgD_pinfty_fin`, `ereal_cvgD_ninfty_fin`, `ereal_cvgD_pinfty_pinfty`,
+      `ereal_cvgD_ninfty_ninfty`
+  + lemma `ereal_limD`
+- in `normedtype.v`:
+  + lemma `closed_ereal_le_ereal`
+  + lemma `closed_ereal_ge_ereal`
+  + lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`.
+  + `uniformType` structure for `ereal`
+
+### Changed
+
+- in `classical_sets.v`:
+  + the index in `bigcup_set1` generalized from `nat` to some `Type`
+  + lemma `bigcapCU` generalized
+  + lemmas `preimage_setU` and `preimage_setI` are about the `setU` and `setI` (instead of `bigcup` and `bigcap`)
+  + `eqEsubset` changed from an implication to an equality
+- lemma `asboolb` moved from `discrete.v` to `boolp.v`
+- lemma `exists2NP` moved from `discrete.v` to `boolp.v`
+- lemma `neg_or` moved from `discrete.v` to `boolp.v` and renamed to `not_orP`
+- definitions `dep_arrow_choiceClass` and `dep_arrow_pointedType`
+  slightly generalized and moved from `topology.v` to
+  `classical_sets.v`
+- the types of the topological notions for `numFieldType` have been moved from `normedtype.v` to `topology.v`
+- the topology of extended real numbers has been moved from `normedtype.v` to `ereal.v` (including the notions of filters)
+- `numdFieldType_lalgType` in `normedtype.v` renamed to `numFieldType_lalgType` in `topology.v`
+- in `ereal.v`:
+  + the first argument of `real_of_er` is now maximal implicit
+  + the first argument of `is_real` is now maximal implicit
+  + generalization of `lee_sum`
+- in `boolp.v`:
+  + rename `exists2NP` to `forall2NP` and make it bidirectionnal
+- moved the definition of `{nngnum _}` and the related bigmax theory to the new `nngnum.v` file
+
+### Renamed
+
+- in `classical_sets.v`:
+  + `setIDl` -> `setIUl`
+  + `setUDl` -> `setUIl`
+  + `setUDr` -> `setUIr`
+  + `setIDr` -> `setIUl`
+  + `setCE` -> `setTD`
+  + `preimage_setU` -> `preimage_bigcup`, `preimage_setI` -> `preimage_bigcap`
+- in `boolp.v`:
+  + `contrap` -> `contra_not`
+  + `contrapL` -> `contraPnot`
+  + `contrapR` -> `contra_notP`
+  + `contrapLR` -> `contraPP`
+
+### Removed
+
+- in `boolp.v`:
+  + `contrapNN`, `contrapTN`, `contrapNT`, `contrapTT`
+  + `eqNN`
+- in `normedtype.v`:
+  + `forallN`
+  + `eqNNP`
+  + `existsN`
+- in `discrete.v`:
+  + `existsP`
+  + `existsNP`
+- in `topology.v`:
+  + `close_to`
+  + `close_cluster`, which is subsumed by `closeEnbhs`
 
 ## [0.3.2] - 2020-08-11
 

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -4,134 +4,12 @@
 
 ### Added
 
-- in `boolp.v`:
-  + lemma `not_andP`
-- in `classical_sets.v`:
-  + lemmas `setIIl`, `setIIr`, `setCS`, `setSD`, `setDS`, `setDSS`, `setCI`,
-    `setDUr`, `setDUl`, `setIDA`, `setDD`
-  + definition `dep_arrow_choiceType`
-  + lemma `bigcup_set0`
-  + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `subsetPset`, `properPset`
-  + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType`
-  + lemma `not_exists2P`
-
-- in `normedtype.v`:
-  + lemma `closed_ereal_le_ereal`
-  + lemma `closed_ereal_ge_ereal`
-  + lemmas `set0M`, `setM0`, `image_set0_set0`, `subset_set1`, `preimage_set0`
-  + lemmas `setICr`, `setUidPl`, `subsets_disjoint`, `disjoints_subset`, `setDidPl`,
-    `setIidPl`, `setIS`, `setSI`, `setISS`, `bigcup_recl`, `bigcup_distrr`,
-    `setMT`
-- in `ereal.v`:
-  + notation `\+` (`ereal_scope`) for function addition
-  + notations `>` and `>=` for comparison of extended real numbers
-  + definition `is_real`, lemmas `is_realN`, `is_realD`, `ERFin_real_of_er`
-  + basic lemmas: `addooe`, `adde_Neq_pinfty`, `adde_Neq_ninfty`, `addERFin`,
-    `subERFin`, `real_of_erN`, `lb_ereal_inf_adherent`
-  + arithmetic lemmas: `oppeD`, `subre_ge0`, `suber_ge0`, `lee_add2lE`, `lte_add2lE`,
-    `lte_add`, `lte_addl`, `lte_le_add`, `lte_subl_addl`, `lee_subr_addr`,
-    `lee_subl_addr`, `lte_spaddr`
-  + lemmas `gee0P`, `sume_ge0`, `lee_sum_nneg`, `lee_sum_nneg_ord`, `lee_sum_nneg_subset`, `lee_sum_nneg_subfset`
-  + lemma `lee_addr`
-  + lemma `lee_adde`
-- in `normedtype.v`:
-  + lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`.
-  + `uniformType` structure for `ereal`
-- in `sequences.v`:
-  + definitions `arithmetic`, `geometric`, `geometric_invn`
-  + lemmas `increasing_series`, `cvg_shiftS`, `mulrn_arithmetic`,
-    `exprn_geometric`, `cvg_arithmetic`, `cvg_expr`,
-    `geometric_seriesE`, `cvg_geometric_series`,
-    `is_cvg_geometric_series`.
-  + lemmas `ereal_cvgN`, `ereal_cvg_ge0`, `ereal_lim_ge`, `ereal_lim_le`
-  + lemma `ereal_cvg_real`
-  + lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series`, `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty`
-  + lemmas `ereal_cvgPpinfty`, `ereal_cvgPninfty`, `lee_lim`
-  + lemma `ereal_cvgD`
-    * with intermediate lemmas `ereal_cvgD_pinfty_fin`, `ereal_cvgD_ninfty_fin`, `ereal_cvgD_pinfty_pinfty`, `ereal_cvgD_ninfty_ninfty`
-  + lemma `ereal_limD`
-- in `classical_sets.v`:
-  + new lemmas: `lb_set1`, `ub_lb_set1`, `ub_lb_refl`, `lb_ub_lb`
-  + new definitions and lemmas: `infimums`, `infimum`, `infimums_set1`, `is_subset1_infimum`
-  + new lemmas: `ge_supremum_Nmem`, `le_infimum_Nmem`, `nat_supremums_neq0`
-  + lemmas `ereal_nbhs_pinfty_ge`, `ereal_nbhs_ninfty_le`
-  + lemma `oppe_continuous`
-  + lemmas `setUCl`, `setDv`
-  + lemmas `image_preimage_subset`, `image_subset`, `preimage_subset`
-  + definition `proper` and its notation `<`
-  + lemmas `setUK`, `setKU`, `setIK`, `setKI`
-  + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `properEneq`
-  + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` on classical `set`.
-- file `nngnum.v`
-
-  + definition `meets` and its notation `#`
-  + lemmas `meetsC`, `meets_openr`, `meets_openl`, `meets_globallyl`,
-    `meets_globallyr `, `meetsxx` and `proper_meetsxx`.
-- in `topology.v`:
-  + definition `limit_point`
-  + lemmas `subset_limit_point`, `closure_limit_point`,
-    `closure_subset`, `closureE`, `closureC`, `closure_id`
-  + lemmas `cluster_nbhs`, `clusterEonbhs`, `closureEcluster`
-  + definition `separated`
-  + lemmas `connected0`, `connectedPn`, `connected_continuous_connected`
-  + lemmas `closureEnbhs`, `closureEonbhs`, `limit_pointEnbhs`,
-    `limit_pointEonbhs`, `closeEnbhs`, `closeEonbhs`.
-
 ### Changed
 
-- in `classical_sets.v`:
-  + the index in `bigcup_set1` generalized from `nat` to some `Type`
-  + lemma `bigcapCU` generalized
-  + lemmas `preimage_setU` and `preimage_setI` are about the `setU` and `setI` (instead of `bigcup` and `bigcap`)
-  + `eqEsubset` changed from an implication to an equality
-- lemma `asboolb` moved from `discrete.v` to `boolp.v`
-- lemma `exists2NP` moved from `discrete.v` to `boolp.v`
-- lemma `neg_or` moved from `discrete.v` to `boolp.v` and renamed to `not_orP`
-- definitions `dep_arrow_choiceClass` and `dep_arrow_pointedType`
-  slightly generalized and moved from `topology.v` to
-  `classical_sets.v`
-- the types of the topological notions for `numFieldType` have been moved from `normedtype.v` to `topology.v`
-- the topology of extended real numbers has been moved from `normedtype.v` to `ereal.v` (including the notions of filters)
-- `numdFieldType_lalgType` in `normedtype.v` renamed to `numFieldType_lalgType` in `topology.v`
-- in `ereal.v`:
-  + the first argument of `real_of_er` is now maximal implicit
-  + the first argument of `is_real` is now maximal implicit
-  + generalization of `lee_sum`
-- in `boolp.v`:
-  + rename `exists2NP` to `forall2NP` and make it bidirectionnal
-- moved the definition of `{nngnum _}` and the related bigmax theory to the new `nngnum.v` file
-
 ### Renamed
 
-- in `classical_sets.v`:
-  + `setIDl` -> `setIUl`
-  + `setUDl` -> `setUIl`
-  + `setUDr` -> `setUIr`
-  + `setIDr` -> `setIUl`
-  + `setCE` -> `setTD`
-  + `preimage_setU` -> `preimage_bigcup`, `preimage_setI` -> `preimage_bigcap`
-- in `boolp.v`:
-  + `contrap` -> `contra_not`
-  + `contrapL` -> `contraPnot`
-  + `contrapR` -> `contra_notP`
-  + `contrapLR` -> `contraPP`
-
 ### Removed
 
-- in `boolp.v`:
-  + `contrapNN`, `contrapTN`, `contrapNT`, `contrapTT`
-  + `eqNN`
-- in `normedtype.v`:
-  + `forallN`
-  + `eqNNP`
-  + `existsN`
-- in `discrete.v`:
-  + `existsP`
-  + `existsNP`
-- in `topology.v`:
-  + `close_to`
-  + `close_cluster`, which is subsumed by `closeEnbhs`
-
 ### Infrastructure
 
 ### Misc
diff --git a/INSTALL.md b/INSTALL.md
@@ -45,7 +45,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.2
+$ opam install coq-mathcomp-analysis.0.3.3
 ```
 4. Everytime you want to work in this same context, you need to type
 ```

diff --git a/opam b/opam
@@ -36,5 +36,5 @@ tags: [
   "keyword: topology"
   "keyword: real numbers"
   "logpath: mathcomp.analysis"
-  "date:2020-08-11"
+  "date:2020-11-11"
 ]