diff --git a/CHANGELOG.md b/CHANGELOG.md index ec059944a..2332c751e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,218 @@ # Changelog -Last releases: [[0.3.1] - 2020-06-11](#031---2020-06-11) and [[0.3.0] - 2020-05-26](#030---2020-05-26) +Last releases: [[0.3.2] - 2020-08-11](#032---2020-08-11) and [[0.3.1] - 2020-06-11](#031---2020-06-11) + +## [0.3.2] - 2020-08-11 + +### Added + +- in `boolp.v`, new lemma `andC` +- in `topology.v`: + + new lemma `open_nbhsE` + + `uniformType` a structure for uniform spaces based on entourages + (`entourage`) + + `uniformType` structure on products, matrices, function spaces + + definitions `nbhs_`, `topologyOfEntourageMixin`, `split_ent`, `nbhsP`, + `entourage_set`, `entourage_`, `uniformityOfBallMixin`, `nbhs_ball` + + lemmas `nbhs_E`, `nbhs_entourageE`, `filter_from_entourageE`, + `entourage_refl`, `entourage_filter`, `entourageT`, `entourage_inv`, + `entourage_split_ex`, `split_entP`, `entourage_split_ent`, + `subset_split_ent`, `entourage_split`, `nbhs_entourage`, `cvg_entourageP`, + `cvg_entourage`, `cvg_app_entourageP`, `cvg_mx_entourageP`, + `cvg_fct_entourageP`, `entourage_E`, `entourage_ballE`, + `entourage_from_ballE`, `entourage_ball`, `entourage_proper_filter`, + `open_nbhs_entourage`, `entourage_close` + + `completePseudoMetricType` structure + + `completePseudoMetricType` structure on matrices and function spaces +- in `classical_sets.v`: + + 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`, `adde_undef` + + 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`, `addeAC`, `addeCA` +- 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`. + +### Changed + +- moved from `normedtype.v` to `boolp.v` and renamed: + + `forallN` -> `forallNE` + + `existsN` -> `existsNE` +- `topology.v`: + + `unif_continuous` uses `entourage` + + `pseudoMetricType` inherits from `uniformType` + + `generic_source_filter` and `set_filter_source` use entourages + + `cauchy` is based on entourages and its former version is renamed + `cauchy_ball` + + `completeType` inherits from `uniformType` and not from `pseudoMetricType` +- moved from `posnum.v` to `Rbar.v`: notation `posreal` +- moved from `normedtype.v` to `Rstruct.v`: + + definitions `R_pointedType`, `R_filteredType`, `R_topologicalType`, + `R_uniformType`, `R_pseudoMetricType` + + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, `continuity_ptE`, + `continuity_pt_cvg'`, `continuity_pt_nbhs'`, `nbhs_pt_comp` + + lemmas `close_trans`, `close_cvgxx`, `cvg_closeP` and `close_cluster` are + valid for a `uniformType` + + moved `continuous_withinNx` from `normedType.v` to `topology.v` and + generalised it to `uniformType` +- moved from `measure.v` to `sequences.v` + + `ereal_nondecreasing_series` + + `ereal_nneg_series_lim_ge` (renamed from `series_nneg`) + +### Renamed + +- in `classical_sets.v`, + + `ub` and `lb` are renamed to `ubound` and `lbound` + + new lemmas: + * `setUCr`, `setCE`, `bigcup_set1`, `bigcapCU`, `subset_bigsetU` +- in `boolp.v`, + + `existsPN` -> `not_existsP` + + `forallPN` -> `not_forallP` + + `Nimply` -> `not_implyP` +- in `classical_sets.v`, `ub` and `lb` are renamed to `ubound` and `lbound` +- in `ereal.v`: + + `eadd` -> `adde`, `eopp` -> `oppe` +- in `topology.v`: + + `locally` -> `nbhs` + + `locally_filterE` -> `nbhs_filterE` + + `locally_nearE` -> `nbhs_nearE` + + `Module Export LocallyFilter` -> `Module Export NbhsFilter` + + `locally_simpl` -> `nbhs_simpl` + * three occurrences + + `near_locally` -> `near_nbhs` + + `Module Export NearLocally` -> `Module Export NearNbhs` + + `locally_filter_onE` -> `nbhs_filter_onE` + + `filter_locallyT` -> `filter_nbhsT` + + `Global Instance locally_filter` -> `Global Instance nbhs_filter` + + `Canonical locally_filter_on` -> `Canonical nbhs_filter_on` + + `neigh` -> `open_nbhs` + + `locallyE` -> `nbhsE` + + `locally_singleton` -> `nbhs_singleton` + + `locally_interior` -> `nbhs_interior` + + `neighT` -> `open_nbhsT` + + `neighI` -> `open_nbhsI` + + `neigh_locally` -> `open_nbhs_nbhs` + + `within_locallyW` -> `within_nbhsW` + + `prod_loc_filter` -> `prod_nbhs_filter` + + `prod_loc_singleton` -> `prod_nbhs_singleton` + + `prod_loc_loc` -> `prod_nbhs_nbhs` + + `mx_loc_filter` -> `mx_nbhs_filter` + + `mx_loc_singleton` -> `mx_nbhs_singleton` + + `mx_loc_loc` -> `mx_nbhs_nbhs` + + `locally'` -> `nbhs'` + + `locallyE'` -> `nbhsE'` + + `Global Instance locally'_filter` -> `Global Instance nbhs'_filter` + + `Canonical locally'_filter_on` -> `Canonical nbhs'_filter_on` + + `locally_locally'` -> `nbhs_nbhs'` + + `Global Instance within_locally_proper` -> `Global Instance within_nbhs_proper` + + `locallyP` -> `nbhs_ballP` + + `locally_ball` -> `nbhsx_ballx` + + `neigh_ball` -> `open_nbhs_ball` + + `mx_locally` -> `mx_nbhs` + + `prod_locally` -> `prod_nbhs` + + `Filtered.locally_op` -> `Filtered.nbhs_op` + + `locally_of` -> `nbhs_of` + + `open_of_locally` -> `open_of_nhbs` + + `locally_of_open` -> `nbhs_of_open` + + `locally_` -> `nbhs_ball` + + lemma `locally_ballE` -> `nbhs_ballE` + + `locallyW` -> `nearW` + + `nearW` -> `near_skip_subproof` + + `locally_infty_gt` -> `nbhs_infty_gt` + + `locally_infty_ge` -> `nbhs_infty_ge` + + `cauchy_entouragesP` -> `cauchy_ballP` +- in `normedtype.v`: + + `locallyN` -> `nbhsN` + + `locallyC` -> `nbhsC` + + `locallyC_ball` -> `nbhsC_ball` + + `locally_ex` -> `nbhs_ex` + + `Global Instance Proper_locally'_numFieldType` -> `Global Instance Proper_nbhs'_numFieldType` + + `Global Instance Proper_locally'_realType` -> `Global Instance Proper_nbhs'_realType` + + `ereal_locally'` -> `ereal_nbhs'` + + `ereal_locally` -> `ereal_nbhs` + + `Global Instance ereal_locally'_filter` -> `Global Instance ereal_nbhs'_filter` + + `Global Instance ereal_locally_filter` -> `Global Instance ereal_nbhs_filter` + + `ereal_loc_singleton` -> `ereal_nbhs_singleton` + + `ereal_loc_loc` -> `ereal_nbhs_nbhs` + + `locallyNe` -> `nbhsNe` + + `locallyNKe` -> `nbhsNKe` + + `locally_oo_up_e1` -> `nbhs_oo_up_e1` + + `locally_oo_down_e1` -> `nbhs_oo_down_e1` + + `locally_oo_up_1e` -> `nbhs_oo_up_1e` + + `locally_oo_down_1e` -> `nbhs_oo_down_1e` + + `locally_fin_out_above` -> `nbhs_fin_out_above` + + `locally_fin_out_below` -> `nbhs_fin_out_below` + + `locally_fin_out_above_below` -> `nbhs_fin_out_above_below` + + `locally_fin_inbound` -> `nbhs_fin_inbound` + + `ereal_locallyE` -> `ereal_nbhsE` + + `locally_le_locally_norm` -> `nbhs_le_locally_norm` + + `locally_norm_le_locally` -> `locally_norm_le_nbhs` + + `locally_locally_norm` -> `nbhs_locally_norm` + + `filter_from_norm_locally` -> `filter_from_norm_nbhs` + + `locally_ball_norm` -> `nbhs_ball_norm` + + `locally_simpl` -> `nbhs_simpl` + + `Global Instance filter_locally` -> `Global Instance filter_locally` + + `locally_interval` -> `nbhs_interval` + + `ereal_locally'_le` -> `ereal_nbhs'_le` + + `ereal_locally'_le_finite` -> `ereal_nbhs'_le_finite` + + `locally_image_ERFin` -> `nbhs_image_ERFin` + + `locally_open_ereal_lt` -> `nbhs_open_ereal_lt` + + `locally_open_ereal_gt` -> `nbhs_open_ereal_gt` + + `locally_open_ereal_pinfty` -> `nbhs_open_ereal_pinfty` + + `locally_open_ereal_ninfty` -> `nbhs_open_ereal_ninfty` + + `continuity_pt_locally` -> `continuity_pt_nbhs` + + `continuity_pt_locally'` -> `continuity_pt_nbhs'` + + `nbhs_le_locally_norm` -> `nbhs_le_nbhs_norm` + + `locally_norm_le_nbhs` -> `nbhs_norm_le_nbhs` + + `nbhs_locally_norm` -> `nbhs_nbhs_norm` + + `locally_normP` -> `nbhs_normP` + + `locally_normE` -> `nbhs_normE` + + `near_locally_norm` -> `near_nbhs_norm` + + lemma `locally_norm_ball_norm` -> `nbhs_norm_ball_norm` + + `locally_norm_ball` -> `nbhs_norm_ball` + + `pinfty_locally` -> `pinfty_nbhs` + + `ninfty_locally` -> `ninfty_nbhs` + + lemma `locally_pinfty_gt` -> `nbhs_pinfty_gt` + + lemma `locally_pinfty_ge` -> `nbhs_pinfty_ge` + + lemma `locally_pinfty_gt_real` -> `nbhs_pinfty_gt_real` + + lemma `locally_pinfty_ge_real` -> `nbhs_pinfty_ge_real` + + `locally_minfty_lt` -> `nbhs_minfty_lt` + + `locally_minfty_le` -> `nbhs_minfty_le` + + `locally_minfty_lt_real` -> `nbhs_minfty_lt_real` + + `locally_minfty_le_real` -> `nbhs_minfty_le_real` + + `lt_ereal_locally` -> `lt_ereal_nbhs` + + `locally_pt_comp` -> `nbhs_pt_comp` +- in `derive.v`: + + `derivable_locally` -> `derivable_nbhs` + + `derivable_locallyP` -> `derivable_nbhsP` + + `derivable_locallyx` -> `derivable_nbhsx` + + `derivable_locallyxP` -> `derivable_nbhsxP` +- in `sequences.v`, + + `cvg_comp_subn` -> `cvg_centern`, + + `cvg_comp_addn` -> `cvg_shiftn`, + + `telescoping` -> `telescope` + + `sderiv1_series` -> `seriesSB` + + `telescopingS0` -> `eq_sum_telescope` + +### Removed + +- in `topology.v`: + + definitions `entourages`, `topologyOfBallMixin`, `ball_set` + + lemmas `locally_E`, `entourages_filter`, `cvg_cauchy_ex` ## [0.3.1] - 2020-06-11 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fd68837e4..c1ee5bdc8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,214 +4,12 @@ ### Added -- in `boolp.v`, new lemma `andC` -- in `topology.v`: - + new lemma `open_nbhsE` - + `uniformType` a structure for uniform spaces based on entourages - (`entourage`) - + `uniformType` structure on products, matrices, function spaces - + definitions `nbhs_`, `topologyOfEntourageMixin`, `split_ent`, `nbhsP`, - `entourage_set`, `entourage_`, `uniformityOfBallMixin`, `nbhs_ball` - + lemmas `nbhs_E`, `nbhs_entourageE`, `filter_from_entourageE`, - `entourage_refl`, `entourage_filter`, `entourageT`, `entourage_inv`, - `entourage_split_ex`, `split_entP`, `entourage_split_ent`, - `subset_split_ent`, `entourage_split`, `nbhs_entourage`, `cvg_entourageP`, - `cvg_entourage`, `cvg_app_entourageP`, `cvg_mx_entourageP`, - `cvg_fct_entourageP`, `entourage_E`, `entourage_ballE`, - `entourage_from_ballE`, `entourage_ball`, `entourage_proper_filter`, - `open_nbhs_entourage`, `entourage_close` - + `completePseudoMetricType` structure - + `completePseudoMetricType` structure on matrices and function spaces -- in `classical_sets.v`: - + 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`, `adde_undef` - + 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`, `addeAC`, `addeCA` -- 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`. - ### Changed -- moved from `normedtype.v` to `boolp.v` and renamed: - + `forallN` -> `forallNE` - + `existsN` -> `existsNE` -- `topology.v`: - + `unif_continuous` uses `entourage` - + `pseudoMetricType` inherits from `uniformType` - + `generic_source_filter` and `set_filter_source` use entourages - + `cauchy` is based on entourages and its former version is renamed - `cauchy_ball` - + `completeType` inherits from `uniformType` and not from `pseudoMetricType` -- moved from `posnum.v` to `Rbar.v`: notation `posreal` -- moved from `normedtype.v` to `Rstruct.v`: - + definitions `R_pointedType`, `R_filteredType`, `R_topologicalType`, - `R_uniformType`, `R_pseudoMetricType` - + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, `continuity_ptE`, - `continuity_pt_cvg'`, `continuity_pt_nbhs'`, `nbhs_pt_comp` - + lemmas `close_trans`, `close_cvgxx`, `cvg_closeP` and `close_cluster` are - valid for a `uniformType` - + moved `continuous_withinNx` from `normedType.v` to `topology.v` and - generalised it to `uniformType` -- moved from `measure.v` to `sequences.v` - + `ereal_nondecreasing_series` - + `ereal_nneg_series_lim_ge` (renamed from `series_nneg`) - ### Renamed -- in `classical_sets.v`, - + `ub` and `lb` are renamed to `ubound` and `lbound` - + new lemmas: - * `setUCr`, `setCE`, `bigcup_set1`, `bigcapCU`, `subset_bigsetU` -- in `boolp.v`, - + `existsPN` -> `not_existsP` - + `forallPN` -> `not_forallP` - + `Nimply` -> `not_implyP` -- in `classical_sets.v`, `ub` and `lb` are renamed to `ubound` and `lbound` -- in `ereal.v`: - + `eadd` -> `adde`, `eopp` -> `oppe` -- in `topology.v`: - + `locally` -> `nbhs` - + `locally_filterE` -> `nbhs_filterE` - + `locally_nearE` -> `nbhs_nearE` - + `Module Export LocallyFilter` -> `Module Export NbhsFilter` - + `locally_simpl` -> `nbhs_simpl` - * three occurrences - + `near_locally` -> `near_nbhs` - + `Module Export NearLocally` -> `Module Export NearNbhs` - + `locally_filter_onE` -> `nbhs_filter_onE` - + `filter_locallyT` -> `filter_nbhsT` - + `Global Instance locally_filter` -> `Global Instance nbhs_filter` - + `Canonical locally_filter_on` -> `Canonical nbhs_filter_on` - + `neigh` -> `open_nbhs` - + `locallyE` -> `nbhsE` - + `locally_singleton` -> `nbhs_singleton` - + `locally_interior` -> `nbhs_interior` - + `neighT` -> `open_nbhsT` - + `neighI` -> `open_nbhsI` - + `neigh_locally` -> `open_nbhs_nbhs` - + `within_locallyW` -> `within_nbhsW` - + `prod_loc_filter` -> `prod_nbhs_filter` - + `prod_loc_singleton` -> `prod_nbhs_singleton` - + `prod_loc_loc` -> `prod_nbhs_nbhs` - + `mx_loc_filter` -> `mx_nbhs_filter` - + `mx_loc_singleton` -> `mx_nbhs_singleton` - + `mx_loc_loc` -> `mx_nbhs_nbhs` - + `locally'` -> `nbhs'` - + `locallyE'` -> `nbhsE'` - + `Global Instance locally'_filter` -> `Global Instance nbhs'_filter` - + `Canonical locally'_filter_on` -> `Canonical nbhs'_filter_on` - + `locally_locally'` -> `nbhs_nbhs'` - + `Global Instance within_locally_proper` -> `Global Instance within_nbhs_proper` - + `locallyP` -> `nbhs_ballP` - + `locally_ball` -> `nbhsx_ballx` - + `neigh_ball` -> `open_nbhs_ball` - + `mx_locally` -> `mx_nbhs` - + `prod_locally` -> `prod_nbhs` - + `Filtered.locally_op` -> `Filtered.nbhs_op` - + `locally_of` -> `nbhs_of` - + `open_of_locally` -> `open_of_nhbs` - + `locally_of_open` -> `nbhs_of_open` - + `locally_` -> `nbhs_ball` - + lemma `locally_ballE` -> `nbhs_ballE` - + `locallyW` -> `nearW` - + `nearW` -> `near_skip_subproof` - + `locally_infty_gt` -> `nbhs_infty_gt` - + `locally_infty_ge` -> `nbhs_infty_ge` - + `cauchy_entouragesP` -> `cauchy_ballP` -- in `normedtype.v`: - + `locallyN` -> `nbhsN` - + `locallyC` -> `nbhsC` - + `locallyC_ball` -> `nbhsC_ball` - + `locally_ex` -> `nbhs_ex` - + `Global Instance Proper_locally'_numFieldType` -> `Global Instance Proper_nbhs'_numFieldType` - + `Global Instance Proper_locally'_realType` -> `Global Instance Proper_nbhs'_realType` - + `ereal_locally'` -> `ereal_nbhs'` - + `ereal_locally` -> `ereal_nbhs` - + `Global Instance ereal_locally'_filter` -> `Global Instance ereal_nbhs'_filter` - + `Global Instance ereal_locally_filter` -> `Global Instance ereal_nbhs_filter` - + `ereal_loc_singleton` -> `ereal_nbhs_singleton` - + `ereal_loc_loc` -> `ereal_nbhs_nbhs` - + `locallyNe` -> `nbhsNe` - + `locallyNKe` -> `nbhsNKe` - + `locally_oo_up_e1` -> `nbhs_oo_up_e1` - + `locally_oo_down_e1` -> `nbhs_oo_down_e1` - + `locally_oo_up_1e` -> `nbhs_oo_up_1e` - + `locally_oo_down_1e` -> `nbhs_oo_down_1e` - + `locally_fin_out_above` -> `nbhs_fin_out_above` - + `locally_fin_out_below` -> `nbhs_fin_out_below` - + `locally_fin_out_above_below` -> `nbhs_fin_out_above_below` - + `locally_fin_inbound` -> `nbhs_fin_inbound` - + `ereal_locallyE` -> `ereal_nbhsE` - + `locally_le_locally_norm` -> `nbhs_le_locally_norm` - + `locally_norm_le_locally` -> `locally_norm_le_nbhs` - + `locally_locally_norm` -> `nbhs_locally_norm` - + `filter_from_norm_locally` -> `filter_from_norm_nbhs` - + `locally_ball_norm` -> `nbhs_ball_norm` - + `locally_simpl` -> `nbhs_simpl` - + `Global Instance filter_locally` -> `Global Instance filter_locally` - + `locally_interval` -> `nbhs_interval` - + `ereal_locally'_le` -> `ereal_nbhs'_le` - + `ereal_locally'_le_finite` -> `ereal_nbhs'_le_finite` - + `locally_image_ERFin` -> `nbhs_image_ERFin` - + `locally_open_ereal_lt` -> `nbhs_open_ereal_lt` - + `locally_open_ereal_gt` -> `nbhs_open_ereal_gt` - + `locally_open_ereal_pinfty` -> `nbhs_open_ereal_pinfty` - + `locally_open_ereal_ninfty` -> `nbhs_open_ereal_ninfty` - + `continuity_pt_locally` -> `continuity_pt_nbhs` - + `continuity_pt_locally'` -> `continuity_pt_nbhs'` - + `nbhs_le_locally_norm` -> `nbhs_le_nbhs_norm` - + `locally_norm_le_nbhs` -> `nbhs_norm_le_nbhs` - + `nbhs_locally_norm` -> `nbhs_nbhs_norm` - + `locally_normP` -> `nbhs_normP` - + `locally_normE` -> `nbhs_normE` - + `near_locally_norm` -> `near_nbhs_norm` - + lemma `locally_norm_ball_norm` -> `nbhs_norm_ball_norm` - + `locally_norm_ball` -> `nbhs_norm_ball` - + `pinfty_locally` -> `pinfty_nbhs` - + `ninfty_locally` -> `ninfty_nbhs` - + lemma `locally_pinfty_gt` -> `nbhs_pinfty_gt` - + lemma `locally_pinfty_ge` -> `nbhs_pinfty_ge` - + lemma `locally_pinfty_gt_real` -> `nbhs_pinfty_gt_real` - + lemma `locally_pinfty_ge_real` -> `nbhs_pinfty_ge_real` - + `locally_minfty_lt` -> `nbhs_minfty_lt` - + `locally_minfty_le` -> `nbhs_minfty_le` - + `locally_minfty_lt_real` -> `nbhs_minfty_lt_real` - + `locally_minfty_le_real` -> `nbhs_minfty_le_real` - + `lt_ereal_locally` -> `lt_ereal_nbhs` - + `locally_pt_comp` -> `nbhs_pt_comp` -- in `derive.v`: - + `derivable_locally` -> `derivable_nbhs` - + `derivable_locallyP` -> `derivable_nbhsP` - + `derivable_locallyx` -> `derivable_nbhsx` - + `derivable_locallyxP` -> `derivable_nbhsxP` -- in `sequences.v`, - + `cvg_comp_subn` -> `cvg_centern`, - + `cvg_comp_addn` -> `cvg_shiftn`, - + `telescoping` -> `telescope` - + `sderiv1_series` -> `seriesSB` - + `telescopingS0` -> `eq_sum_telescope` - ### Removed -- in `topology.v`: - + definitions `entourages`, `topologyOfBallMixin`, `ball_set` - + lemmas `locally_E`, `entourages_filter`, `cvg_cauchy_ex` - ### Infrastructure ### Misc