fixes #1297 (#1298)

* fixes #1297
math-comp · Aug 22, 2024 · 7171aaf · 7171aaf
1 parent 8acde98
commit 7171aaf
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git 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
@@ -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).