From c2f685a083ed9de783f2cbea3719b449358ce9b4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 18 Jul 2024 21:32:58 +0900 Subject: [PATCH] fix changelog --- CHANGELOG_UNRELEASED.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ff2fdb9cde..37aef5fa3a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -49,10 +49,6 @@ ### Changed -- in `topology.v`: - + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, - `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned - into local `Let`'s - in `classical_sets.v`: + lemmas `setC_I`, `bigcup_subset` @@ -97,6 +93,11 @@ ### Changed +- in `topology.v`: + + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, + `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned + into local `Let`'s + - in `lebesgue_integral.v`: + lemma `measurable_int`: argument `mu` now explicit