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