From 4044c4bb014999017c98bf71cacc5e390ead83f3 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 4 Mar 2021 20:38:58 +0900 Subject: [PATCH] changelog for version 0.3.6 (#338) * changelog for version 0.3.6 --- CHANGELOG.md | 81 ++++++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 79 ---------------------------------------- INSTALL.md | 2 +- 3 files changed, 81 insertions(+), 81 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9548a9504..a47b58ba8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,85 @@ # Changelog -Last releases: [[0.3.5] - 2020-12-21](#035---2020-12-21) and [[0.3.4] - 2020-12-12](#034---2020-12-12) +Last releases: [[0.3.6] - 2021-03-04](#036---2021-03-04) and [[0.3.5] - 2020-12-21](#035---2020-12-21) + +## [0.3.6] - 2021-03-04 + +### Added + +- in `boolp.v`: + + lemmas `iff_notr`, `iff_not2` +- in `classical_sets.v`: + + lemmas `subset_has_lbound`, `subset_has_ubound` + + lemma `mksetE` + + definitions `cover`, `partition`, `pblock_index`, `pblock` + + lemmas `trivIsetP`, `trivIset_sets`, `trivIset_restr`, `perm_eq_trivIset` + + lemma `fdisjoint_cset` + + lemmas `setDT`, `set0D`, `setD0` + + lemmas `setC_bigcup`, `setC_bigcap` +- in `reals.v`: + + lemmas `sup_setU`, `inf_setU` + + lemmas `RtointN`, `floor_le0` + + definition `Rceil`, lemmas `isint_Rceil`, `Rceil0`, `le_Rceil`, `Rceil_le`, `Rceil_ge0` + + definition `ceil`, lemmas `RceilE`, `ceil_ge0`, `ceil_le0` +- in `ereal.v`: + + lemmas `esum_fset_ninfty`, `esum_fset_pinfty`, `esum_pinfty` +- in `normedtype.v`: + + lemmas `ereal_nbhs'_le`, `ereal_nbhs'_le_finite` + + lemmas `ball_open` + + definition `closed_ball_`, lemmas `closed_closed_ball_` + + definition `closed_ball`, lemmas `closed_ballxx`, `closed_ballE`, + `closed_ball_closed`, `closed_ball_subset`, `nbhs_closedballP`, `subset_closed_ball` + + lemmas `nbhs0_lt`, `nbhs'0_lt`, `interior_closed_ballE`, open_nbhs_closed_ball` + + section "LinearContinuousBounded" + * lemmas `linear_boundedP`, `linear_continuous0`, `linear_bounded0`, + `continuousfor0_continuous`, `linear_bounded_continuous`, `bounded_funP` +- in `measure.v`: + + definition `sigma_finite` + +### Changed + +- in `classical_sets.v`: + + generalization and change of `trivIset` (and thus lemmas `trivIset_bigUI` and `trivIset_setI`) + + `bigcup_distrr`, `bigcup_distrl` generalized +- header in `normedtype.v`, precisions on `bounded_fun` +- in `reals.v`: + + `floor_ge0` generalized and renamed to `floorR_ge_int` +- in `ereal.v`, `ereal_scope` notation scope: + + `x <= y` notation changed to `lee (x : er _) (y : er _)` and + `only printing` notation `x <= y` for `lee x y` + + same change for `<` + + change extended to notations `_ <= _ <= _`, `_ < _ <= _`, `_ <= _ < _`, `_ < _ < _` + +### Renamed + +- in `reals.v`: + + `floor` -> `Rfloor` + + `isint_floor` -> `isint_Rfloor` + + `floorE` -> `RfloorE` + + `mem_rg1_floor` -> `mem_rg1_Rfloor` + + `floor_ler` -> `Rfloor_ler` + + `floorS_gtr` -> `RfloorS_gtr` + + `floor_natz` -> `Rfloor_natz` + + `Rfloor` -> `Rfloor0` + + `floor1` -> `Rfloor1` + + `ler_floor` -> `ler_Rfloor` + + `floor_le0` -> `Rfloor_le0` + + `ifloor` -> `floor` + + `ifloor_ge0` -> `floor_ge0` +- in `topology.v`: + + `ball_ler` -> `le_ball` +- in `normedtype.v`, `bounded_on` -> `bounded_near` +- in `measure.v`: + + `AdditiveMeasure.Measure` -> `AdditiveMeasure.Axioms` + + `OuterMeasure.OuterMeasure` -> `OuterMeasure.Axioms` + +### Removed +- in `topology.v`: + + `ball_le` +- in `classical_sets.v`: + + lemma `bigcapCU` +- in `sequences.v`: + + lemmas `ler_sum_nat`, `sumr_const_nat` ## [0.3.5] - 2020-12-21 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5cfd1c73b..5a426cd4b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,92 +3,13 @@ ## [Unreleased] ### Added - -- in `normedtype.v`, lemmas `ereal_nbhs'_le`, `ereal_nbhs'_le_finite` - -- in `normedtype.v`, lemmas `ball_open` - -- in `normedtype.v`, definition `closed_ball_`, lemmas `closed_closed_ball_` - -- in `normedtype.v`, definition `closed_ball`, lemmas `closed_ballxx`, `closed_ballE`, - `closed_ball_closed`, `closed_ball_subset`, `nbhs_closedballP`, `subset_closed_ball` - -- in `normedtype.v`, lemmas `nbhs0_lt`, `nbhs'0_lt`, `interior_closed_ballE`, open_nbhs_closed_ball` -- in `classical_sets.v`, lemmas `subset_has_lbound`, `subset_has_ubound` - -- in `classical_sets.v`, lemma `mksetE` - -- in `classical_sets.v`: - + definitions `cover`, `partition`, `pblock_index`, `pblock` - + lemmas `trivIsetP`, `trivIset_sets`, `trivIset_restr`, `perm_eq_trivIset` - + lemma `fdisjoint_cset` - -- in `reals.v`, lemmas `sup_setU`, `inf_setU` -- in `boolp.v`, lemmas `iff_notr`, `iff_not2` -- in `reals.v`, lemmas `RtointN`, `floor_le0` -- in `reals.v`, definition `Rceil`, lemmas `isint_Rceil`, `Rceil0`, `le_Rceil`, - `Rceil_le`, `Rceil_ge0` -- in `reals.v`, definition `ceil`, lemmas `RceilE`, `ceil_ge0`, `ceil_le0` - -- in `ereal.v`, lemmas `esum_fset_ninfty`, `esum_fset_pinfty`, `esum_pinfty` -- in `classical_sets.v`, lemmas `setDT`, `set0D`, `setD0` -- in `classical_sets.v`, lemmas `setC_bigcup`, `setC_bigcap` - -- in `measure.v`, definition `sigma_finite` - -- in `normedtype.v`: section "LinearContinuousBounded" - + lemmas `linear_boundedP`, `linear_continuous0`, `linear_bounded0`, - `continuousfor0_continuous`, `linear_bounded_continuous`, `bounded_funP` ### Changed -- header in `normedtype.v`, precisions on `bounded_fun` -- in `reals.v`: - + `floor_ge0` generalized and renamed to `floorR_ge_int` -- in `ereal.v`, `ereal_scope` notation scope: - + `x <= y` notation changed to `lee (x : er _) (y : er _)` and - `only printing` notation `x <= y` for `lee x y` - + same change for `<` - + change extended to notations `_ <= _ <= _`, `_ < _ <= _`, `_ <= _ < _`, `_ < _ < _` - -- in `classical_sets.v`: - + generalization and change of `trivIset` (and thus lemmas `trivIset_bigUI` and `trivIset_setI`) - -- in `classical_sets.v`: - + `bigcup_distrr`, `bigcup_distrl` generalized - ### Renamed -- in `normedtype.v`, `bounded_on` -> `bounded_near` - -- in `topology.v`, `ball_ler` -> `le_ball` -- in `reals.v`: - + `floor` -> `Rfloor` - + `isint_floor` -> `isint_Rfloor` - + `floorE` -> `RfloorE` - + `mem_rg1_floor` -> `mem_rg1_Rfloor` - + `floor_ler` -> `Rfloor_ler` - + `floorS_gtr` -> `RfloorS_gtr` - + `floor_natz` -> `Rfloor_natz` - + `Rfloor` -> `Rfloor0` - + `floor1` -> `Rfloor1` - + `ler_floor` -> `ler_Rfloor` - + `floor_le0` -> `Rfloor_le0` - + `ifloor` -> `floor` - + `ifloor_ge0` -> `floor_ge0` - -- in `measure.v`: - + `AdditiveMeasure.Measure` -> `AdditiveMeasure.Axioms` - + `OuterMeasure.OuterMeasure` -> `OuterMeasure.Axioms` - ### Removed -- in `topology.v`: - + `ball_le` -- in `classical_sets.v`, lemma `bigcapCU` - -- in `sequences.v`, lemmas `ler_sum_nat`, `sumr_const_nat` - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index b16d5179b..980af57ba 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.3.5 +$ opam install coq-mathcomp-analysis.0.3.6 ``` 4. Everytime you want to work in this same context, you need to type ```