fixes #1301

- add relation_scope

CHANGELOG_UNRELEASED.md

@@ -28,6 +28,10 @@
   + lemmas `outer_measure_open_itv_cover`, `outer_measure_open_le`,
     `outer_measure_open`, `outer_measure_Gdelta`, `negligible_outer_measure`
 
+- in `classical_sets.v`:
+  + scope `relation_scope` with delimiter `relation`
+  + notation `^-1` in `relation_scope` (use to be a local notation)
+
 ### Changed
 
 - in `normedtype.v`:

classical/classical_sets.v

@@ -206,7 +206,7 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*                                                                            *)
 (* ## Composition of relations                                                *)
 (* ```                                                                        *)
-(*                A \; B == [set x | exists z, A (x.1, z) & B (z, x.2)]       *)
+(*                B \; A == [set x | exists z, A (x.1, z) & B (z, x.2)]       *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -3335,8 +3335,15 @@ Notation notin_xsectionM := notin_xsectionX (only parsing).
 #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to notin_ysectionX.")]
 Notation notin_ysectionM := notin_ysectionX (only parsing).
 
+Declare Scope relation_scope.
+Delimit Scope relation_scope with relation.
+
 Notation "B \; A" :=
-  ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : classical_set_scope.
+  ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : relation_scope.
+
+Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : relation_scope.
+
+Local Open Scope relation_scope.
 
 Lemma set_compose_subset {X Y : Type} (A C : set (X * Y)) (B D : set (Y * X)) :
   A `<=` C -> B `<=` D -> A \; B `<=` C \; D.
@@ -3350,3 +3357,5 @@ Proof.
 rewrite eqEsubset; split => [[_ _] [_ [_ _ [<- <-//]]]|[x y] Exy]/=.
 by exists x => //; exists x.
 Qed.
+
+Local Close Scope relation_scope.

theories/function_spaces.v

@@ -99,8 +99,6 @@ Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.
-
 (** Product topology, also known as the topology of pointwise convergence *)
 Section Product_Topology.
 
@@ -401,6 +399,7 @@ End product_spaces.
 
 (**md the uniform topologies type *)
 Section fct_Uniform.
+Local Open Scope relation_scope.
 Variables (T : choiceType) (U : uniformType).
 
 Definition fct_ent := filter_from (@entourage U)
@@ -420,10 +419,10 @@ move=> [B entB sBA] fg feg; apply/sBA => t; rewrite feg.
 exact: entourage_refl.
 Qed.
 
-Lemma fct_ent_inv A : fct_ent A -> fct_ent (A^-1)%classic.
+Lemma fct_ent_inv A : fct_ent A -> fct_ent A^-1.
 Proof.
-move=> [B entB sBA]; exists (B^-1)%classic; first exact: entourage_inv.
-by move=> fg Bgf; apply/sBA.
+move=> [B entB sBA]; exists B^-1; first exact: entourage_inv.
+by move=> fg Bgf; exact/sBA.
 Qed.
 
 Lemma fct_ent_split A : fct_ent A -> exists2 B, fct_ent B & B \; B `<=` A.
@@ -469,7 +468,7 @@ apply/cvg_ex; exists (fun t => lim (@^~t @ F)).
 apply/cvg_fct_entourageP => A entA; near=> f => t; near F => g.
 apply: (entourage_split (g t)) => //; first by near: g; apply: cvF.
 move: (t); near: g; near: f; apply: nearP_dep; apply: Fc.
-exists ((split_ent A)^-1)%classic=> //=.
+by exists (split_ent A)^-1%relation => /=.
 Unshelve. all: by end_near. Qed.
 
 HB.instance Definition _ := Uniform_isComplete.Build
@@ -531,7 +530,7 @@ near F1 => x1; near=> x2; apply: (entourage_split (h x1)) => //.
   by apply/xsectionP; near: x1; exact: hl.
 apply: (entourage_split (f x1 x2)) => //.
   by apply/xsectionP; near: x2; exact: fh.
-move: (x2); near: x1; have /cvg_fct_entourageP /(_ (_^-1%classic)):= fg; apply.
+move: (x2); near: x1; have /cvg_fct_entourageP /(_ _^-1%relation):= fg; apply.
 exact: entourage_inv.
 Unshelve. all: by end_near. Qed.
 
@@ -546,10 +545,10 @@ rewrite !near_simpl -near2_pair near_map2; near=> x1 y1 => /=; near F2 => x2.
 apply: (entourage_split (f x1 x2)) => //.
   by apply/xsectionP; near: x2; exact: fh.
 apply: (entourage_split (f y1 x2)) => //; last first.
-  apply/xsectionP; near: x2; apply/(fh _ (xsection ((_^-1)%classic) _)).
+  apply/xsectionP; near: x2; apply/(fh _ (xsection _^-1%relation _)).
   exact: nbhs_entourage (entourage_inv _).
 apply: (entourage_split (g x2)) => //; move: (x2); [near: x1|near: y1].
-  have /cvg_fct_entourageP /(_ (_^-1)%classic) := fg; apply.
+  have /cvg_fct_entourageP /(_ _^-1%relation) := fg; apply.
   exact: entourage_inv.
 by have /cvg_fct_entourageP := fg; apply.
 Unshelve. all: by end_near. Qed.
@@ -1031,7 +1030,7 @@ apply: (entourage_split (g x)) => //.
   by near: g; apply/Ff/uniform_nbhs; exists (split_ent A); split => // ?; exact.
 apply: (entourage_split (g y)) => //; near: y; near: g.
   by apply: (filterS _ ctsF) => g /(_ x) /cvg_app_entourageP; exact.
-apply/Ff/uniform_nbhs; exists (split_ent (split_ent A))^-1%classic.
+apply/Ff/uniform_nbhs; exists (split_ent (split_ent A))^-1%relation.
 by split; [exact: entourage_inv | move=> g fg; near_simpl; near=> z; exact: fg].
 Unshelve. all: end_near. Qed.
 

theories/normedtype.v

@@ -3537,13 +3537,12 @@ Lemma uniform_separatorW {T : uniformType} (A B : set T) :
 Proof. by case=> E entE AB0; exists (Uniform.class T), E; split => // ?. Qed.
 
 Section Urysohn.
+Local Open Scope relation_scope.
 Context {T : topologicalType}.
 Hypothesis normalT : normal_space T.
 Section normal_uniform_separators.
 Context (A : set T).
 
-Local Notation "A ^-1" := [set xy | A (xy.2, xy.1)] : classical_set_scope.
-
 (* Urysohn's lemma guarantees a continuous function : T -> R
    where "f @` A = [set 0]" and "f @` B = [set 1]".
    The idea is to leverage countable_uniformity to build that function
@@ -3583,7 +3582,7 @@ case: (pselect (R x)); first by left.
 by move/subsetC: LR => /[apply] => ?; right.
 Qed.
 
-Local Lemma ury_base_inv E : ury_base E -> ury_base (E^-1)%classic.
+Local Lemma ury_base_inv E : ury_base E -> ury_base E^-1.
 Proof.
 case; case=> L R ? <-; exists (L, R) => //.
 by rewrite eqEsubset; split => //; (case=> x y [] [? ?]; [left| right]).
@@ -3622,10 +3621,10 @@ move/(_ (globally [set fg | fg.1 = fg.2])); apply; split.
 exact: ury_base_refl.
 Qed.
 
-Local Lemma set_prod_invK (K : set (T * T)) : (K^-1^-1)%classic = K.
+Local Lemma set_prod_invK (K : set (T * T)) : K^-1^-1 = K.
 Proof. by rewrite eqEsubset; split; case. Qed.
 
-Local Lemma ury_unif_inv E : ury_unif E -> ury_unif (E^-1)%classic.
+Local Lemma ury_unif_inv E : ury_unif E -> ury_unif E^-1.
 Proof.
 move=> ufE F [/filter_inv FF urF]; have [] := ufE [set (V^-1)%classic | V in F].
   split => // K /ury_base_inv/urF /= ?; exists (K^-1)%classic => //.
@@ -3635,7 +3634,7 @@ Qed.
 
 Local Lemma ury_unif_split_iter E n :
   filterI_iter ury_base n E -> exists2 K : set (T * T),
-    filterI_iter ury_base n.+1 K & K\;K `<=` E.
+    filterI_iter ury_base n.+1 K & K \; K `<=` E.
 Proof.
 elim: n E; first move=> E [].
 - move=> ->; exists setT => //; exists setT; first by left.
@@ -4745,7 +4744,7 @@ set B := [set x | exists2 E : {fset I}, {subset E <= D} &
 set A := `[a, b] `&` B.
 suff Aeab : A = `[a, b]%classic.
   suff [_ [E ? []]] : A b by exists E.
-  by rewrite Aeab/= inE/=; apply/andP.
+  by rewrite Aeab/= inE/=; exact/andP.
 apply: segment_connected.
 - have aba : a \in `[a, b] by rewrite in_itv /= lexx.
   exists a; split=> //; have /sabUf [i /= Di fia] := aba.
@@ -5206,18 +5205,18 @@ Lemma closed_ball_closed (R : realFieldType) (V : pseudoMetricType R) (x : V)
 Proof. exact: closed_closure. Qed.
 
 Lemma closed_ball_itv (R : realFieldType) (x r : R) : 0 < r ->
-  (closed_ball x r = `[x - r, x + r]%classic)%R.
+  closed_ball x r = `[x - r, x + r]%classic.
 Proof.
 by move=> r0; apply/seteqP; split => y;
   rewrite closed_ballE// /closed_ball_ /= in_itv/= ler_distlC.
 Qed.
 
-Lemma closed_ball_ball {R : realFieldType} (x r : R) : (0 < r)%R ->
-  closed_ball x r = [set (x - r)%R] `|` ball x r `|` [set (x + r)%R].
+Lemma closed_ball_ball {R : realFieldType} (x r : R) : 0 < r ->
+  closed_ball x r = [set x - r] `|` ball x r `|` [set x + r].
 Proof.
-move=> r0; rewrite closed_ball_itv// -(@setU1itv _ _ _ (x - r)%R); last first.
+move=> r0; rewrite closed_ball_itv// -(@setU1itv _ _ _ (x - r)); last first.
   by rewrite bnd_simp lerBlDr -addrA lerDl ltW// addr_gt0.
-rewrite -(@setUitv1 _ _ _ (x + r)%R); last first.
+rewrite -(@setUitv1 _ _ _ (x + r)); last first.
   by rewrite bnd_simp ltrBlDr -addrA ltrDl addr_gt0.
 by rewrite ball_itv setUA.
 Qed.
@@ -5237,7 +5236,7 @@ by move=> m xm; rewrite -ball_normE /ball_ /= (le_lt_trans _ r01).
 Qed.
 
 Lemma nbhs_closedballP (R : realFieldType) (M : normedModType R) (B : set M)
-  (x : M) : nbhs x B <-> exists (r : {posnum R}), closed_ball x r%:num `<=` B.
+  (x : M) : nbhs x B <-> exists r : {posnum R}, closed_ball x r%:num `<=` B.
 Proof.
 split=> [/nbhs_ballP[_/posnumP[r] xrB]|[e xeB]]; last first.
   apply/nbhs_ballP; exists e%:num => //=.
@@ -5252,7 +5251,7 @@ Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V)
 Proof. exact: subset_closure. Qed.
 
 Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M)
-    (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
+  (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
 Proof.
 move=> aA Ax.
 have /(@nbhs_closedballP R M _ x)[r xrA]: nbhs x A by rewrite nbhsE/=; exists A.
@@ -5428,7 +5427,6 @@ Qed.
 End image_interval.
 
 Section LinearContinuousBounded.
-
 Variables (R : numFieldType) (V W : normedModType R).
 
 Lemma linear_boundedP (f : {linear V -> W}) : bounded_near f (nbhs 0) <->
@@ -5482,7 +5480,7 @@ Lemma linear_bounded_continuous (f : {linear V -> W}) :
   bounded_near f (nbhs 0) <-> continuous f.
 Proof.
 split; first exact: bounded_linear_continuous.
-by move=> /(_ 0); apply: continuous_linear_bounded.
+by move=> /(_ 0); exact: continuous_linear_bounded.
 Qed.
 
 Lemma bounded_funP (f : {linear V -> W}) :
@@ -5494,7 +5492,7 @@ split => [/(_ 1) [M Bf]|/linear_boundedP fr y].
   by rewrite sub0r normrN => x1; exact/Bf/ltW.
 near +oo_R => r; exists (r * y) => x xe.
 rewrite (@le_trans _ _ (r * `|x|)) //; first by move: {xe} x; near: r.
-by rewrite ler_pM //.
+by rewrite ler_pM.
 Unshelve. all: by end_near. Qed.
 
 End LinearContinuousBounded.