generalize pushforward

math-comp · Jul 13, 2022 · d02104b · d02104b
1 parent d46de60
commit d02104b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -17,6 +17,8 @@
 - in `ereal.v`:
   + generalize `lee_pmul`
   + simplify `lte_le_add`, `lte_le_dadd`, `lte_le_sub`, `lte_le_dsub`
+- in `measure.v`:
+  + generalize `pushforward`
 
 ### Renamed
 

diff --git a/theories/measure.v b/theories/measure.v
@@ -1466,7 +1466,8 @@ Arguments measure_bigcup {d R T} mu A.
 
 Section pushforward_measure.
 Local Open Scope ereal_scope.
-Variables (d : measure_display) (T1 T2 : measurableType d) (f : T1 -> T2).
+Variables (d d' : measure_display).
+Variables (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2).
 Hypothesis mf : measurable_fun setT f.
 Variables (R : realFieldType) (m : {measure set T1 -> \bar R}).