rebase

Author: Tragicus

CHANGELOG_UNRELEASED.md

@@ -6,72 +6,6 @@
 
 - in `realfun.v`:
   + lemma `derivable_sqrt`
-- in `topology_structure.v`
-  + lemma `interiorS`
-
-- in `order_topology.v`
-  + lemma `itv_closed_ends_closed`
-- in `classical_sets.v`
-  + lemma `in_set1_eq`
-
-- in `set_interval.v`
-  + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
-
-- in `Rstruct.v`:
-  + lemmas `R0E` and `R1E`
-  + multirule `RealsE` to convert from Stdlib reals to Analysis ones
-
-- in `Rstruct_topology.v`:
-  + lemma `RlnE`
-- in probability.v
-  + lemma `pmf_ge0`
-  + lemmas `pmf_gt0_countable`, `pmf_measurable`
-
-- in `unstable.v`:
-  + lemmas `oppr_itvNy`, `oppr_itvy`
-  + lemmas `ltr_norm_bound`, `real_ltr_bound`, `real_ltrNbound`, `ltr_bound`,
-    `ltrNbound`
-
-- in `set_interval.v`:
-  + lemmas `opp_preimage_itvbndy`, `opp_preimage_itvbndbnd`
-
-- in `lebesgue_measure.v`:
-  + lemma `lebesgue_measure_unique`
-
-- in `lebesgue_integral_nonneg.v`:
-  + lemmas `lebesgue_measureN`, `ge0_integration_by_substitution0`
-
-- in `measurable_realfun.v`:
-  + definition `min_mfun`
-
-- in `random_variable.v`
-  + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`,
-    `le0_expectation_cdf`
-
-- in `lebesgue_integral_nonneg.v`:
-  + lemma `integral_setU`
-
-- in `measurable_realfun.v`:
-  + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`,
-    `emeasurable_fun_itv_cc`
-- in `derive.v`:
-  + lemmas `derivable_mxP`, `derive_mx`
-
-- in `subtype_topology.v`:
-  + lemma `within_continuous_comp`
-
-- in `pseudometric_normed_Zmodule.v`:
-  + lemmas `within_continuousB`, `within_continuousD`
-
-- in `normed_module.v`:
-  + lemma `within_continuous_compN`
-- in `normed_module.v`:
-  + lemma `compact_has_sup`
-
-- in `derive.v`:
-  + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
-- in `tvs.v`
-  + lemmas `cvg_sum`, `sum_continuous`
 
 - in `unstable.v`:
   + structure `Norm`