From 7abf4c87e15e9118a1146ebd914b9c1940a80a64 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 Aug 2024 10:10:32 +0900 Subject: [PATCH 1/2] fixes #1297 --- theories/lebesgue_measure.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 6af5ed6e5d..cb754b1ba8 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1840,8 +1840,8 @@ under eq_fun do rewrite -mulr_natr. by do 2 apply: measurable_funM => //. Qed. -Lemma measurable_funX {R : realType} D (f : R -> R) n : measurable_fun D f -> - measurable_fun D (fun x => f x ^+ n). +Lemma measurable_funX d (T : measurableType d) {R : realType} D (f : T -> R) n : + measurable_fun D f -> measurable_fun D (fun x => f x ^+ n). Proof. move=> mf. exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). From 2b82cee0ac04d7a10042aad832dc29b4b7c6b87c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 Aug 2024 10:13:18 +0900 Subject: [PATCH 2/2] changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 916dc2336f..16b83b1abf 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -60,6 +60,9 @@ - in `derive.v`: + lemma `derivable_cst` +- in `lebesgue_measure.v`: + + lemma `measurable_funX` (was `measurable_fun_pow`) + ### Deprecated ### Removed