From f2887237dd2b7b9292cca054cff5ef58b88edbf6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 11 Jun 2021 23:54:29 +0900 Subject: [PATCH] changelog 0.3.8.1 --- CHANGELOG.md | 28 ++++++++++++++++++++++++++-- CHANGELOG_UNRELEASED.md | 6 ------ 2 files changed, 26 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cc4f017dd..89691664f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,27 @@ # Changelog -Last releases: [[0.3.8] - 2021-06-01](#038---2021-06-01) and [[0.3.7] - 2021-04-01](#037---2021-04-01) +Last releases: [[0.3.8.1] - 2021-06-12](#0381---2021-06-12) and [[0.3.8] - 2021-06-01](#038---2021-06-01) + +## [0.3.8.1] - 2021-06-12 + +### Added + +- in `sequences.v`: + + lemma `dvg_harmonic` +- in `classical_sets.v`: + + definitions `image`, `image2` + +### Changed + +- in `classical_sets.v` + + notations `[set E | x in A]` and `[set E | x in A & y in B]` + now use definitions `image` and `image2` resp. + + notation ``f @` A`` now uses the definition `image` + +### Removed + +- in `sequences.v`: + + lemma `iter_addr` ## [0.3.8] - 2021-06-01 @@ -89,7 +110,9 @@ Last releases: [[0.3.8] - 2021-06-01](#038---2021-06-01) and [[0.3.7] - 2021-04- ### Changed -- in `classical_sets.v`, lemma `subset_bigsetU` +- in `classical_sets.v` + + lemma `subset_bigsetU` + + notation ``f @` A`` defined as `[set f x | x in A]` instead of using `image` - in `ereal.v`: + change implicits of lemma `lee_sum_nneg_ord` + `ereal_sup_ninfty` and `ereal_inf_pinfty` made equivalences @@ -144,6 +167,7 @@ Last releases: [[0.3.8] - 2021-06-01](#038---2021-06-01) and [[0.3.7] - 2021-04- - in `classical_sets.v` + lemmas `eq_set_inl`, `set_in_in` + + definition `image` - from `topology.v`: + lemmas `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`, `can_mono_in`, `onW_can`, `onW_can_in`, `in_onW_can`, diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 761a6ee82..c1ee5bdc8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,18 +4,12 @@ ### Added -- in `sequences.v`: - + lemma `dvg_harmonic` - ### Changed ### Renamed ### Removed -- in `sequences.v`: - + lemma `iter_addr` - ### Infrastructure ### Misc