restrain the scope of measurable args (#1116)

Co-authored-by: Kazuhiko Sakaguchi <[email protected]>
math-comp · Jan 9, 2024 · 75650ef · 75650ef
1 parent 1fd0e85
commit 75650ef
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 8 deletions.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -494,24 +494,24 @@ Qed.
 
 Lemma measurable_itv (i : interval R) : measurable [set` i].
 Proof.
-have moc (a b : R) : measurable `]a, b]%classic.
+have moc (a b : R) : measurable `]a, b].
   by apply: sub_sigma_algebra; apply: is_ocitv.
-have mopoo (x : R) : measurable `]x, +oo[%classic.
+have mopoo (x : R) : measurable `]x, +oo[.
   by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable.
-have mnooc (x : R) : measurable `]-oo, x]%classic.
+have mnooc (x : R) : measurable `]-oo, x].
   by rewrite -setCitvr; exact/measurableC.
-have ooE (a b : R) : `]a, b[%classic = `]a, b]%classic `\ b.
+have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b.
   case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D.
   by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
-have moo (a b : R) : measurable `]a, b[%classic.
+have moo (a b : R) : measurable `]a, b[.
   by rewrite ooE; exact: measurableD.
-have mcc (a b : R) : measurable `[a, b]%classic.
+have mcc (a b : R) : measurable `[a, b].
   case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
   by rewrite -setU1itv//; apply/measurableU.
-have mco (a b : R) : measurable `[a, b[%classic.
+have mco (a b : R) : measurable `[a, b[.
   case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
   by rewrite -setU1itv//; apply/measurableU.
-have oooE (b : R) : `]-oo, b[%classic = `]-oo, b]%classic `\ b.
+have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
   by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
 case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
 - by rewrite -setU1itv//; exact/measurableU.

diff --git a/theories/measure.v b/theories/measure.v
@@ -723,6 +723,8 @@ HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
 HB.structure Definition SemiRingOfSets d :=
   {T of Pointed T & isSemiRingOfSets d T}.
 
+Arguments measurable {d}%measure_display_scope {s} _%classical_set_scope.
+
 Lemma measurable_curry (T1 T2 : Type) d (T : semiRingOfSetsType d)
     (G : T1 * T2 -> set T) (x : T1 * T2) :
   measurable (G x) <-> measurable (curry G x.1 x.2).