From 7171aaf77ac6cadf8177c3478fbf16e5ba79c822 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Thu, 22 Aug 2024 11:12:34 +0900
Subject: [PATCH] fixes #1297 (#1298)

* fixes #1297
---
 CHANGELOG_UNRELEASED.md     | 3 +++
 theories/lebesgue_measure.v | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 916dc2336..16b83b1ab 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
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 6af5ed6e5..cb754b1ba 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).