From 3de3c6e2e861f5cd145278e3299ef73572ac6282 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 29 Jul 2024 20:00:50 +0900 Subject: [PATCH] changelog --- CHANGELOG_UNRELEASED.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index af62a5f2d..894b37d94 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -110,6 +110,8 @@ `parameterized_integral_left`, `parameterized_integral_cvg_at_left`, `parameterized_integral_continuous` + corollary `continuous_FTC2` +- in `classical_sets.v`: + + lemmas `xsectionP`, `ysectionP` ### Changed @@ -238,6 +240,9 @@ + lemmas `floor0`, `floor1` + lemma `le_floor` (use `Num.Theory.floor_le` instead) +- in `topology.v`, `function_spaces.v`, `normedtype.v`: + + local notation `to_set` + ### Infrastructure ### Misc