changelog for version 1.7.0

CHANGELOG.md

@@ -1,6 +1,220 @@
 # Changelog
 
-Latest releases: [[1.6.0] - 2024-10-25](#160---2024-10-25) and [[1.5.0] - 2024-10-09](#150---2024-10-09)
+Latest releases: [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25)
+
+## [1.7.0] - 2024-11-22
+
+### Added
+
+- package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`
+  with files
+  + `constructive_ereal.v`
+  + `reals.v`
+  + `real_interval.v`
+  + `signed.v`
+  + `itv.v`
+  + `prodnormedzmodule.v`
+  + `nsatz_realtype.v`
+  + `all_reals.v`
+
+- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals`
+  with files
+  + `xfinmap.v`
+  + `discrete.v`
+  + `realseq.v`
+  + `realsum.v`
+  + `distr.v`
+
+- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals`
+  with file
+  + `Rstruct.v`
+
+- package `coq-mathcomp-analysis-stdlib` depending on
+  `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files
+  + new file `Rstruct_topology.v`
+  + `showcase/uniform_bigO.v`
+
+- in file `mathcomp_extra.v`,
+  + new definition `sigT_fun`.
+  + definition `idempotent_fun`
+
+- in `boolp.v`:
+  + lemmas `existT_inj1`, `surjective_existT`
+  + lemma `existT_inj2`
+  + new lemmas `uncurryK`, and `curryK`
+
+- new file `topology_theory/one_point_compactification.v`,
+  + new definitions `one_point_compactification`, and `one_point_nbhs`.
+  + new lemmas `one_point_compactification_compact`,
+    `one_point_compactification_some_nbhs`,
+    `one_point_compactification_some_continuous`,
+    `one_point_compactification_open_some`,
+    `one_point_compactification_weak_topology`, and
+    `one_point_compactification_hausdorff`.
+
+- new file `topology_theory/sigT_topology.v`,
+  + new definition `sigT_nbhs`.
+  + new lemmas `sigT_nbhsE`, `existT_continuous`, `existT_open_map`,
+    `existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and
+    `sigT_compact`.
+
+- in file `topology_theory/product_topology.v`,
+  + new lemmas `swap_continuous`, `prodA_continuous`, and
+    `prodAr_continuous`.
+
+- in file `topology_theory/order_topology.v`
+  + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
+    `max_fun_continuous`.
+
+- in file `topology_theory/weak_topology.v`,
+  + new lemma `continuous_comp_weak`
+
+- in `topology_theory/topology_structure.v`:
+  + definitions `regopen`, `regclosed`
+  + lemmas `closure_setC`, `interiorC`, `closureU`, `interiorU`,
+           `closureEbigcap`, `interiorEbigcup`,
+	   `closure_open_regclosed`, `interior_closed_regopen`,
+	   `closure_interior_idem`, `interior_closure_idem`
+  + mixin `isContinuous`, type `continuousType`, structure `Continuous`
+  + new lemma `continuousEP`.
+  + new definition `mkcts`.
+
+- in file `topology_theory/subspace_topology.v`,
+  + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and
+    `continuous_subspace_prodP`.
+  + type `continuousFunType`, HB structure `ContinuousFun`
+
+- in file `topology_theory/subtype_topology.v`,
+  + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`,
+    `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
+    `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.
+
+- in file `separation_axioms.v`,
+  + new lemmas `compact_normal_local`, and `compact_normal`.
+  + new lemma `sigT_hausdorff`.
+
+- in file `function_spaces.v`,
+  + new definition `eval`
+  + new lemmas `continuous_curry_fun`, `continuous_curry_cvg`,
+    `eval_continuous`, and `compose_continuous`
+
+- new file `tvs.v`:
+  + HB structures `NbhsNmodule`, `NbhsZmodule`, `NbhsLmodule`, `TopologicalNmodule`,
+    `TopologicalZmodule`
+  + notation `topologicalLmoduleType`, HB structure `TopologicalLmodule`
+  + HB structures `UniformZmodule`, `UniformLmodule`
+  + definition `convex`
+  + mixin `Uniform_isTvs`
+  + type `tvsType`, HB.structure `Tvs`
+  + HB.factory `TopologicalLmod_isTvs`
+  + lemma `nbhs0N`
+  + lemma `nbhsN`
+  + lemma `nbhsT`
+  + lemma `nbhsB`
+  + lemma `nbhs0Z`
+  + lemma `nbhZ`
+
+- in file `normedtype.v`,
+  + new definition `type` (in module `completely_regular_uniformity`)
+  + new lemmas `normal_completely_regular`,
+    `one_point_compactification_completely_reg`,
+    `nbhs_one_point_compactification_weakE`,
+    `locally_compact_completely_regular`, and
+    `completely_regular_regular`.
+  + new lemmas `near_in_itvoy`, `near_in_itvNyo`
+
+- in `measure.v`:
+  + lemma `countable_measurable`
+
+- in `realfun.v`:
+  + lemma `cvgr_dnbhsP`
+  + new definitions `prodA`, and `prodAr`.
+  + new lemmas `prodAK`, `prodArK`, and `swapK`.
+
+- new file `homotopy_theory/path.v`,
+  + new definitions `reparameterize`, `mk_path`, and `chain_path`.
+  + new lemmas `path_eqP`, and `chain_path_cts_point`.
+
+- new file `homotopy_theory/wedge_sigT.v`,
+  + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`.
+  + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`,
+    `wedge_liftE`, `wedge_openP`,
+    `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`,
+    `wedge_compact`, `wedge_connected`.
+  + new definitions `wedge_fun`, and `wedge_prod`.
+  + new lemmas `wedge_fun_continuous`, `wedge_lift_funE`,
+    `wedge_fun_comp`, `wedge_prod_pointE`, `wedge_prod_inj`,
+    `wedge_prod_continuous`, `wedge_prod_open`, `wedge_hausdorff`, and
+    `wedge_fun_joint_continuous`.
+  + new definition `bpwedge_shared_pt`.
+  + new notations `bpwedge`, and `bpwedge_lift`.
+
+- new file `homotopy_theory/homotopy.v`
+
+### Changed
+
+- moved from `Rstruct.v` to `Rstruct_topology.v`
+  + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`,
+    `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs`
+    and `nbhs_pt_comp`
+
+- moved from `real_interval.v` to `normedtype.v`
+  + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
+    `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
+    `disj_itv_Rhull`
+
+- in `topology.v`:
+  + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
+    `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
+	into local `Let`'s
+
+- in file `normedtype.v`,
+  + changed `completely_regular_space` to depend on uniform separators
+    which removes the dependency on `R`.  The old formulation can be
+    recovered easily with `uniform_separatorP`.
+  + HB structure `normedModule` now depends on a Tvs
+    instead of a Lmodule
+  + Factory `PseudoMetricNormedZmod_Lmodule_isNormedModule` becomes
+    `PseudoMetricNormedZmod_Tvs_isNormedModule`
+  + Section `prod_NormedModule` now depends on a `numFieldType`
+
+- in `lebesgue_integral.v`:
+  + structure `SimpleFun` now inside a module `HBSimple`
+  + structure `NonNegSimpleFun` now inside a module `HBNNSimple`
+  + lemma `cst_nnfun_subproof` has now a different statement
+  + lemma `indic_nnfun_subproof` has now a different statement
+
+### Renamed
+
+- in `normedtype.v`:
+  + `near_in_itv` -> `near_in_itvoo`
+  + Section `regular_topology` to `standard_topology`
+
+### Generalized
+
+- in `lebesgue_integral.v`:
+  + generalized from `sigmaRingType`/`realType` to `sigmaRingType`/`sigmaRingType`
+    * mixin `isMeasurableFun`
+    * structure `MeasurableFun`
+	* definition `mfun`
+    * lemmas `mfun_rect`, `mfun_valP`, `mfuneqP`
+
+### Deprecated
+
+- in `topology_theory/topology_structure.v`:
+  + lemma `closureC`
+
+### Removed
+
+- in `cardinality.v`:
+  + lemma `cst_fimfun_subproof`
+
+- in `lebesgue_integral.v`:
+  + definition `cst_mfun`
+  + lemma `mfun_cst`
+  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
+  + lemma `cst_nnfun_subproof` (turned into a `Let`)
+  + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
 
 ## [1.6.0] - 2024-10-25