From 48235eb9858a0d24ab002c4ed93799611f8031dc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 19 Jan 2024 14:15:12 +0900 Subject: [PATCH] fix --- CHANGELOG_UNRELEASED.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d2ddab391..4e62b78dd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -65,15 +65,18 @@ - in `ereal.v`: + lemma `ereal_supy` +- in `mathcomp_extra.v`: + + lemmas `last_filterP`, + `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`, + `path_lt_le_last` + - in file `realfun.v`, + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, `variation`, `variations`, `bounded_variation`, `total_variation`, `neg_tv`, and `pos_tv`. + new lemmas `left_right_continuousP`, - `nondecreasing_funN`, `nonincreasing_funN`, `last_filterP`, - `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`, - `path_lt_le_last` + `nondecreasing_funN`, `nonincreasing_funN` + new lemmas `itv_partition_nil`, `itv_partition_cons`, `itv_partition1`, `itv_partition_size_neq0`, `itv_partitionxx`, `itv_partition_le`,