renaming

CHANGELOG_UNRELEASED.md

@@ -14,10 +14,21 @@
   + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`,
     `derivable_horner`, `derivE`, `continuous_horner`
   + instance `is_derive_poly`
-- in `mathcomp_extra.v`:
-  + lemma `partition_disjoint_bigfcup`
-- in `lebesgue_measure.v`:
-  + lemma `measurable_indicP`
+
+- in `lebesgue_integral.v`:
+  + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral`
+
+- new file `pi_irrational.v`:
+  + lemmas `measurable_poly`
+  + definition `rational`
+  + module `pi_irrational`
+  + lemma `pi_irrationnal`
+
+- in `numfun.v`
+  + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
+
+- in `classical_sets.v`:
+  + lemmas `xsectionE`, `ysectionE`
 
 - in `numfun.v`:
   + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
@@ -29,47 +40,26 @@
 
 - in `measure.v`:
   + lemma `preimage_class_comp`
-  + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`,
-    notations `.-mapping`, `.-mapping.-measurable`
+  + defintions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`,
+    notations `.-preimage`, `.-preimage.-measurable`
 
 - in `lebesgue_measure.v`:
   + lemmas `measurable_funrpos`, `measurable_funrneg`
 
-- in `lebesgue_integral.v`:
-  + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral`
-
-- new file `pi_irrational.v`:
-  + lemmas `measurable_poly`
-  + definition `rational`
-  + module `pi_irrational`
-  + lemma `pi_irrationnal`
-- in `constructive_ereal.v`:
-  + notations `\prod` in scope ereal_scope
-  + lemmas `prode_ge0`, `prode_fin_num`
-- in `probability.v`:
-  + lemma `expectation_def`
-  + notation `'M_`
-
 - new file `independence.v`:
   + lemma `expectationM_ge0`
   + definition `independent_events`
   + definition `mutual_independence`
   + definition `independent_RVs`
   + definition `independent_RVs2`
-  + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`,
-    `g_sigma_algebra_mapping_funrneg`
+  + lemmas `g_sigma_algebra_preimage_comp`, `g_sigma_algebra_preimage_funrpos`,
+    `g_sigma_algebra_preimage_funrneg`
   + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`,
     `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`,
     `independent_RVs2_funrpospos`
   + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
     ` expectation_prod`
 
-- in `numfun.v`
-  + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
-
-- in `classical_sets.v`:
-  + lemmas `xsectionE`, `ysectionE`
-
 ### Changed
 
 - in `lebesgue_integrale.v`
@@ -95,33 +85,6 @@
   + `sigma_algebra_image_class` -> `sigma_algebra_image`
   + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE`
   + `preimage_classes_comp` -> `g_sigma_preimageU_comp`
-
-### Renamed
-
-- in `lebesgue_measure.v`:
-  + `measurable_fun_indic` -> `measurable_indic`
-  + `emeasurable_fun_sum` -> `emeasurable_sum`
-  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
-  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
-- in `probability.v`:
-  + `expectationM` -> `expectationZl`
-
-- in `classical_sets.v`:
-  + `preimage_itv_o_infty` -> `preimage_itvoy`
-  + `preimage_itv_c_infty` -> `preimage_itvcy`
-  + `preimage_itv_infty_o` -> `preimage_itvNyo`
-  + `preimage_itv_infty_c` -> `preimage_itvNyc`
-
-- in `constructive_ereal.v`:
-  + `maxeMr` -> `maxe_pMr`
-  + `maxeMl` -> `maxe_pMl`
-  + `mineMr` -> `mine_pMr`
-  + `mineMl` -> `mine_pMl`
-
-- in `probability.v`:
-  + `integral_distribution` -> `ge0_integral_distribution`
-
-- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
 
 ### Generalized
 
@@ -143,38 +106,6 @@
 - in `sequences.v`:
   + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
     `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
-- in `topology_structure.v`:
-  + lemma `closureC`
-
-- in file `lebesgue_integral.v`:
-  + lemma `approximation`
-
-### Removed
-
-- in `lebesgue_integral.v`:
-  + definition `cst_mfun`
-  + lemma `mfun_cst`
-
-- in `cardinality.v`:
-  + lemma `cst_fimfun_subproof`
-
-- in `lebesgue_integral.v`:
-  + 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)
-
-- in `lebesgue_integral.v`:
-  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
-  + notation `measurable_fun_indic` (deprecation since 0.6.3)
-- in `constructive_ereal.v`
-  + notation `lee_opp` (deprecated since 0.6.5)
-  + notation `lte_opp` (deprecated since 0.6.5)
-- in `measure.v`:
-  + `dynkin_setI_bigsetI` (use `big_ind` instead)
-
-- in `lebesgue_measurable.v`:
-  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
-  + notation `measurable_power_pos` (deprecated since 0.6.4)
 
 ### Infrastructure