fixes math-comp#1248

classical/classical_sets.v

@@ -3217,9 +3217,15 @@ Proof. by move=> x Axy; exists y; rewrite /ysection/= inE in Axy. Qed.
 Lemma mem_xsection x y A : (y \in xsection A x) = ((x, y) \in A).
 Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /xsection !inE /= inE]. Qed.
 
+Lemma xsectionP x y A : xsection A x y <-> A (x, y).
+Proof. by rewrite /xsection/= inE. Qed.
+
 Lemma mem_ysection x y A : (x \in ysection A y) = ((x, y) \in A).
 Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed.
 
+Lemma ysectionP x y A : ysection A y x <-> A (x, y).
+Proof. by rewrite /ysection/= inE. Qed.
+
 Lemma xsection0 x : xsection set0 x = set0.
 Proof. by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed.
 

theories/cantor.v

@@ -397,29 +397,29 @@ Let ent_balls' (E : set (T * T)) :
   exists M : set (set T), entourage E -> [/\
     finite_set M,
     forall A, M A -> exists a, A a /\
-      A `<=` closure [set y | split_ent E (a, y)],
+      A `<=` closure (xsection (split_ent E) a),
     exists A B : set T, M A /\ M B /\ A != B,
     \bigcup_(A in M) A = [set: T] &
     M `<=` closed].
 Proof.
 have [entE|?] := pselect (entourage E); last by exists point.
 move: cptT; rewrite compact_cover.
-pose fs x := interior [set y | split_ent E (x, y)].
+pose fs x := interior (xsection (split_ent E) x).
 move=> /(_ T [ set: T] fs)[t _|t _ |].
 - exact: open_interior.
-- exists t => //.
-  by rewrite /fs /interior -nbhs_entourageE; exists (split_ent E).
+- exists t => //; rewrite /fs /interior.
+  by rewrite -nbhs_entourageE; exists (split_ent E) => // ? /xsectionP.
 move=> M' _ Mcov; exists
   ((closure \o fs) @` [set` M'] `|` [set [set t0]; [set t1]]).
 move=> _; split=> [|A [|]| | |].
 - rewrite finite_setU; split; first exact/finite_image/finite_fset.
   exact: finite_set2.
 - move=> [z M'z] <-; exists z; split.
   + apply: subset_closure; apply: nbhs_singleton; apply: nbhs_interior.
-    by rewrite -nbhs_entourageE; exists (split_ent E).
+      by rewrite -nbhs_entourageE; exists (split_ent E) => // t /xsectionP.
   + by apply: closure_subset; exact: interior_subset.
 - by case => ->; [exists t0 | exists t1]; split => // t ->;
-    apply: subset_closure; exact: entourage_refl.
+    apply/subset_closure/xsectionP; exact: entourage_refl.
 - exists [set t0], [set t1]; split;[|split].
   + by right; left.
   + by right; right.
@@ -512,10 +512,11 @@ have [//| | |? []//| |? []// | |] := @tree_map_props
       by move=> ? [? ?] [? ?]; exists (existT _ _ ebC).
     case: pselect; last by move => ? ? [].
     by move=> e _ [? ?] [? ?]; exists (projT1 (cid e)).
-  suff : E (x, y) by move/ExU; move/eqP/disjoints_subset: UVI0 => /[apply].
+  suff : E (x, y).
+    by move/xsectionP/ExU; move/eqP/disjoints_subset: UVI0 => /[apply].
   have [z [Dz DzE]] := Csub _ cbD.
-  have /ent_closure:= DzE _ Dx => /(_ (ent_count_unif n))/ctE [_ /= Exz].
-  have /ent_closure:= DzE _ Dy => /(_ (ent_count_unif n))/ctE [Ezy _].
+  have /ent_closure := DzE _ Dx => /(_ (ent_count_unif n))/xsectionP/ctE [_ /= Exz].
+  have /ent_closure := DzE _ Dy => /(_ (ent_count_unif n))/xsectionP/ctE [Ezy _].
   exact: (@entourage_split _ (*[the uniformType of T]*) z).
 by move=> f [ctsf surjf _]; exists f.
 Qed.

theories/ereal.v

@@ -1263,7 +1263,7 @@ rewrite predeq2E => x A; split.
       rewrite /= /e' lt_min; apply/andP; split.
         by rewrite subr_gt0 lt_contract lte_fin ltrBlDr ltrDl.
       by rewrite subr_gt0 lt_contract lte_fin ltrDl.
-    case=> [r' /= re'r'| |]/=.
+    case=> [r' /= /xsectionP/= re'r'| |]/=.
     * rewrite /ereal_ball in re'r'.
       have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E).
         apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //.
@@ -1287,7 +1287,7 @@ rewrite predeq2E => x A; split.
         by rewrite ltrBlDr subrK.
       rewrite ltrBlDr -lte_fin -(contractK (_ + r)%:E)%R.
       by rewrite addrC -(contractK r'%:E) // lt_expand ?inE ?contract_le1.
-    * rewrite /ereal_ball [contract +oo]/=.
+    * move=> /xsectionP/=; rewrite /ereal_ball [contract +oo]/=.
       rewrite lt_min => /andP[re'1 re'2].
       have [cr0|cr0] := lerP 0 (contract r%:E).
         move: re'2; rewrite ler0_norm; last first.
@@ -1302,7 +1302,7 @@ rewrite predeq2E => x A; split.
       exfalso.
       move: h; apply/negP; rewrite -leNgt.
       by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)).
-    * rewrite /ereal_ball [contract -oo]/=; rewrite opprK.
+    * move=> /xsectionP/=; rewrite /ereal_ball [contract -oo]/= opprK.
       rewrite lt_min => /andP[re'1 _].
       move: re'1.
       rewrite ger0_norm; last first.
@@ -1315,7 +1315,7 @@ rewrite predeq2E => x A; split.
   + exists (diag (1 - contract M%:E))%R; rewrite /diag.
       exists (1 - contract M%:E)%R => //=.
       by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm.
-    case=> [r| |]/=.
+    case=> [r| |]/= /xsectionP/=.
     * rewrite /ereal_ball [_ +oo]/= => rM1.
       apply: MA; rewrite lte_fin.
       rewrite ger0_norm in rM1; last first.
@@ -1334,10 +1334,9 @@ rewrite predeq2E => x A; split.
       exists (1 + contract M%:E)%R => //=.
       rewrite -ltrBlDl sub0r.
       by move: (contract_lt1 M); rewrite ltr_norml => /andP[].
-    case=> [r| |].
+    case=> [r| |] /xsectionP/=.
     * rewrite /ereal_ball => /= rM1.
-      apply MA.
-      rewrite lte_fin.
+      apply: MA; rewrite lte_fin.
       rewrite ler0_norm in rM1; last first.
         rewrite lerBlDl addr0 ltW //.
         by move: (contract_lt1 r); rewrite ltr_norml => /andP[].
@@ -1352,13 +1351,14 @@ rewrite predeq2E => x A; split.
     * rewrite /ereal_ball /= => _; exact: MA.
 - case: x => [r [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA] |
                [E [_/posnumP[e] reA] sEA]] //=.
-  + by apply nbhs_fin_inbound with e => ? ?; exact/sEA/reA.
+  + by apply nbhs_fin_inbound with e => ? ?; exact/sEA/xsectionP/reA.
   + have [|] := boolP (e%:num <= 1)%R.
-      by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/reA.
-    by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/reA.
+      by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/xsectionP/reA.
+    by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/xsectionP/reA.
   + have [|] := boolP (e%:num <= 1)%R.
-      by move/nbhs_oo_down_e1; apply => ? ?; exact/sEA/reA.
-    by rewrite -ltNge => /nbhs_oo_down_1e; apply => ? ?; exact/sEA/reA.
+      move/nbhs_oo_down_e1; apply => ? ?; apply: sEA.
+      by rewrite /xsection/= inE; exact: reA.
+    by rewrite -ltNge =>/nbhs_oo_down_1e; apply => ? ?; exact/sEA/xsectionP/reA.
 Qed.
 
 HB.instance Definition _ := Nbhs_isPseudoMetric.Build R (\bar R)

theories/function_spaces.v

@@ -100,8 +100,6 @@ 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.
-Local Notation "'to_set' A x" := ([set y | A (x, y)])
-  (at level 0, A at level 0) : classical_set_scope.
 
 (** Product topology, also known as the topology of pointwise convergence *)
 Section Product_Topology.
@@ -381,7 +379,7 @@ Qed.
 Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product.
 Proof.
 move=> /accessible_closed_set1 cl1 x y; case: (eqVneq x y) => // xny _ _ jxjy.
-have [] := (@sepf [set y] x (cl1 y)); first by exact/eqP.
+have [] := @sepf [set y] x (cl1 y); first exact/eqP.
 move=> i P; suff : join_product x i != join_product y i by rewrite jxjy => /eqP.
 apply/negP; move: P; apply: contra_not => /eqP; rewrite /join_product => ->.
 by apply: subset_closure; exists y.
@@ -532,9 +530,9 @@ Lemma cvg_switch_1 {U : uniformType}
 Proof.
 move=> fg fh hl; apply/cvg_app_entourageP => A entA.
 near F1 => x1; near=> x2; apply: (entourage_split (h x1)) => //.
-  by near: x1; apply/(hl (to_set _ l)) => /=.
+  by apply/xsectionP; near: x1; exact: hl.
 apply: (entourage_split (f x1 x2)) => //.
-  by near: x2; apply/(fh x1 (to_set _ _)) => /=.
+  by apply/xsectionP; near: x2; exact: fh.
 move: (x2); near: x1; have /cvg_fct_entourageP /(_ (_^-1%classic)):= fg; apply.
 exact: entourage_inv.
 Unshelve. all: by end_near. Qed.
@@ -548,9 +546,9 @@ Proof.
 move=> fg fh; apply: cauchy_cvg => A entA.
 rewrite !near_simpl -near2_pair near_map2; near=> x1 y1 => /=; near F2 => x2.
 apply: (entourage_split (f x1 x2)) => //.
-  by near: x2; apply/(fh _ (to_set _ _)) => /=.
+  by apply/xsectionP; near: x2; exact: fh.
 apply: (entourage_split (f y1 x2)) => //; last first.
-  near: x2; apply/(fh _ (to_set ((_^-1)%classic) _)).
+  apply/xsectionP; near: x2; apply/(fh _ (xsection ((_^-1)%classic) _)).
   exact: nbhs_entourage (entourage_inv _).
 apply: (entourage_split (g x2)) => //; move: (x2); [near: x1|near: y1].
   have /cvg_fct_entourageP /(_ (_^-1)%classic) := fg; apply.
@@ -595,13 +593,15 @@ Proof.
 split=> [[Q [[/= W oW <- /=] Wf subP]]|[E [entE subP]]].
   rewrite openE /= /interior in oW.
   case: (oW _ Wf) => ? [ /= E entE] Esub subW.
-  exists E; split=> // h Eh; apply/subP/subW/Esub => /= [[u Au]].
+  exists E; split=> // h Eh; apply/subP/subW/xsectionP/Esub => /= [[u Au]].
   by apply: Eh => /=; rewrite -inE.
 near=> g; apply: subP => y /mem_set Ay; rewrite -!(sigLE A).
 move: (SigSub _); near: g.
 have := (@cvg_image _ _ (@sigL_arrow _ A V) _ f (nbhs_filter f)
   (image_sigL point)).1 cvg_id [set h | forall y, E (sigL A f y, h y)].
-case; first by exists [set fg | forall y, E (fg.1 y, fg.2 y)]; [exists E|].
+case.
+  exists [set fg | forall y, E (fg.1 y, fg.2 y)] => //; first by exists E.
+  by move=> g /xsectionP.
 move=> B nbhsB rBrE; apply: (filterS _ nbhsB) => g Bg [y yA].
 by move: rBrE; rewrite eqEsubset; case => [+ _]; apply; exists g.
 Unshelve. all: by end_near. Qed.
@@ -656,10 +656,10 @@ Proof.
 move=> FF; rewrite propeqE; split.
   move=> + W => /(_ [set t | W (t x)]) +; rewrite -nbhs_entourageE.
   rewrite uniform_nbhs => + [Q entQ subW].
-  by apply; exists Q; split => // h Qf; exact/subW/Qf.
+  by apply; exists Q; split => // h Qf; exact/subW/xsectionP/Qf.
 move=> Ff W; rewrite uniform_nbhs => [[E] [entE subW]].
 apply: (filterS subW); move/(nbhs_entourage (f x))/Ff: entE => //=; near_simpl.
-by apply: filter_app; apply: nearW=> ? ? ? ->.
+by apply: filter_app; apply: nearW=> ? /xsectionP ? ? ->.
 Qed.
 
 Lemma uniform_subset_nbhs (f : U -> V) (A B : set U) :
@@ -721,10 +721,12 @@ move=> hV.
 rewrite propeqE; split; last exact: eq_in_close.
 rewrite entourage_close => C u; rewrite inE => uA; apply: hV.
 rewrite /cluster -nbhs_entourageE /= => X Y [X' eX X'X] [Y' eY Y'Y].
-exists (g u); split; [apply: X'X| apply: Y'Y]; last exact: entourage_refl.
+exists (g u); split; [apply: X'X| apply: Y'Y]; apply/xsectionP; last first.
+  exact: entourage_refl.
 apply: (C [set fg | forall y, A y -> X' (fg.1 y, fg.2 y)]) => //=.
 by rewrite uniform_entourage; exists X'.
 Qed.
+
 Lemma uniform_restrict_cvg
     (F : set_system (U -> V)) (f : U -> V) A : Filter F ->
   {uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
@@ -751,9 +753,9 @@ Proof.
 rewrite eqEsubset; split=> A.
   case/uniform_nbhs => E [entE] /filterS; apply.
   exists [set fh | forall y, E (fh.1 y, fh.2 y)]; first by exists E.
-  by move=> ? /=.
+  by move=> ? /xsectionP /=.
 case => J [E entE EJ] /filterS; apply; apply/uniform_nbhs; exists E.
-by split => // z /= Efz; apply: EJ => t /=; exact: Efz.
+by split => // z /= Efz; apply/xsectionP/EJ => t /=; exact: Efz.
 Qed.
 
 Lemma cvg_uniformU (f : U -> V) (F : set_system (U -> V)) A B : Filter F ->
@@ -842,13 +844,14 @@ near=> z => /=; (suff: A `<=` [set y | O (z y)] by exact); near: z.
 apply: cfA => x Ax; have : O (f x) by exact: fAO.
 move: (oO); rewrite openE /= => /[apply] /[dup] /ctsf Ofx /=.
 rewrite /interior -nbhs_entourageE => -[E entE EfO].
-exists (f @^-1` to_set (split_ent E) (f x),
+exists (f @^-1` xsection (split_ent E) (f x),
     [set g | forall w, A w -> split_ent E (f w, g w)]).
   split => //=; last exact: fam_nbhs.
   by apply: ctsf; rewrite /= -nbhs_entourageE; exists (split_ent E).
-case=> y g [/= Efxy] AEg Ay; apply: EfO; apply: subset_split_ent => //.
-by exists (f y) => //=; exact: AEg.
+case=> y g [/= /xsectionP Efxy] AEg Ay; apply/EfO/xsectionP.
+by apply: subset_split_ent => //; exists (f y) => //=; exact: AEg.
 Unshelve. all: by end_near. Qed.
+
 End FamilyConvergence.
 
 (**md It turns out `{family compact, U -> V}` can be generalized to only assume
@@ -962,13 +965,13 @@ move=> ctsf FF; split; first last.
 move/compact_open_cvgP=> cptOF; apply/cvg_sup => -[K cptK R].
 case=> D [[E oE <-] Ekf] /filterS; apply.
 move: oE; rewrite openE => /(_ _ Ekf); case => A [J entJ] EKR KfE.
-near=> z; apply/KfE/EKR => -[u Kp]; rewrite /sigL_arrow /= /set_val /= /eqincl.
+near=> z; apply/KfE/xsectionP/EKR => -[u Kp]; rewrite /sigL_arrow /= /set_val /= /eqincl.
 (have Ku : K u by rewrite inE in Kp); move: u Ku {D Kp}; near: z.
 move/compact_near_coveringP/near_covering_withinP : (cptK); apply.
 move=> u Ku; near (powerset_filter_from (@entourage V)) => E'.
 have entE' : entourage E' by exact: (near (near_small_set _)).
-pose C := f @^-1` to_set E' (f u).
-pose B := \bigcup_(z in K `&` closure C) interior (to_set E' (f z)).
+pose C := f @^-1` xsection E' (f u).
+pose B := \bigcup_(z in K `&` closure C) interior (xsection E' (f z)).
 have oB : open B by apply: bigcup_open => ? ?; exact: open_interior.
 have fKB : f @` (K `&` closure C) `<=` B.
   move=> _ [z KCz <-]; exists z => //; rewrite /interior.
@@ -982,14 +985,19 @@ exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]).
 case=> z h /= [Cz KB Kz].
 case: (KB (h z)); first by exists z; split => //; exact: subset_closure.
 move=> w [Kw Cw /interior_subset Jfwhz]; apply: subset_split_ent => //.
-exists (f w); last apply: (near (small_ent_sub _) E') => //.
+exists (f w); last first.
+  apply: (near (small_ent_sub _) E') => //.
+  exact/xsectionP.
 apply: subset_split_ent => //; exists (f u).
-  by apply/entourage_sym; apply: (near (small_ent_sub _) E').
-have [] := Cw (f@^-1` (to_set E' (f w))).
+  apply/entourage_sym; apply: (near (small_ent_sub _) E') => //.
+  exact/xsectionP.
+have [] := Cw (f @^-1` xsection E' (f w)).
   by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'.
 move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r).
-  exact: (near (small_ent_sub _) E').
-by apply/entourage_sym; apply: (near (small_ent_sub _) E').
+  apply: (near (small_ent_sub _) E') => //.
+  exact/xsectionP.
+apply/entourage_sym; apply: (near (small_ent_sub _) E') => //.
+exact/xsectionP.
 Unshelve. all: by end_near. Qed.
 
 End compact_open_uniform.
@@ -1181,7 +1189,7 @@ Proof.
 move=> entE; have : ({ptws, nbhs f --> f}) by [].
 have ? : Filter (nbhs f) by exact: nbhs_pfilter. (* NB: This Filter (nbhs f) used to infer correctly. *)
 rewrite pointwise_cvg_family_singleton => /fam_cvgP /(_ [set x]).
-rewrite uniform_set1 => /(_ _ (to_set E (f x))); apply; first by exists x.
+rewrite uniform_set1 => /(_ _ [set y | E (f x, y)]); apply; first by exists x.
 by move: E entE; exact/cvg_entourageP.
 Qed.
 
@@ -1285,7 +1293,7 @@ apply: (entourage_split (f x) entE).
   exact: (near (fam_nbhs _ entE' (@compact_set1 _ x)) g).
 apply: (entourage_split (f y) (entourage_split_ent entE)).
   apply: (near (small_ent_sub _) E') => //.
-  by near: y; apply: ((@ctsW f Wf x) (to_set _ _)); exact: nbhs_entourage.
+  by apply/xsectionP; near: y; apply: (@ctsW f Wf x); exact: nbhs_entourage.
 apply: (near (small_ent_sub _) E') => //.
 by apply: (near (fam_nbhs _ entE' cptU) g) => //; exact: (near UWx y).
 Unshelve. all: end_near. Qed.
@@ -1299,14 +1307,16 @@ move=> pcptW ctsW; apply: (equicontinuous_subset_id (@subset_closure _ W)).
 apply: compact_equicontinuous; last by rewrite -precompactE.
 move=> f; rewrite closureEcvg => [[G PG [Gf GW]]] x B /=.
 rewrite -nbhs_entourageE => -[E entE] /filterS; apply; near_simpl.
-suff ctsf : continuous f by move: E entE; apply/cvg_app_entourageP; exact: ctsf.
+suff ctsf : continuous f.
+  near=> x0; apply/xsectionP; near: x0.
+  by move: E entE; apply/cvg_app_entourageP; exact: ctsf.
 apply/continuous_localP => x'; apply/near_powerset_filter_fromP.
   by move=> ? ?; exact: continuous_subspaceW.
 case: (@lcptX x') => // U; rewrite withinET => nbhsU [cptU _].
 exists U => //; apply: (uniform_limit_continuous_subspace PG _ _).
   by near=> g; apply: continuous_subspaceT; near: g; exact: GW.
 by move/fam_cvgP/(_ _ cptU) : Gf.
-Unshelve. end_near. Qed.
+Unshelve. all: end_near. Qed.
 
 End precompact_equicontinuous.
 

theories/lebesgue_integral.v

@@ -6527,12 +6527,12 @@ have locg_B n : locally_integrable [set: R] (g_B n).
       by case: (_ \in _); rewrite ?mulr1 ?mulr0 ?normr0 ?lee_fin.
 have locf_g_B n : locally_integrable setT (f_ k \- g_B n)%R.
   apply: locally_integrableB => //; split.
-  + by move/EFin_measurable_fun : mf.
-  + exact: openT.
-  + move=> K _ cK; rewrite (le_lt_trans _ intf)//=.
+  - by move/EFin_measurable_fun : mf.
+  - exact: openT.
+  - move=> K _ cK; rewrite (le_lt_trans _ intf)//=.
     apply: ge0_subset_integral => //.
-    * exact: compact_measurable.
-    * by do 2 apply: measurableT_comp => //; move/EFin_measurable_fun : mf.
+    + exact: compact_measurable.
+    + by do 2 apply: measurableT_comp => //; move/EFin_measurable_fun : mf.
 have mEHL i : measurable (HLf_g_Be i).
   rewrite /HLf_g_Be -[X in measurable X]setTI.
   apply: emeasurable_fun_o_infty => //.
@@ -6566,7 +6566,7 @@ have davgfEe : B k `&` [set x | (f_ k)^* x > e%:E] `<=` Ee.
   rewrite {1}(splitr e) EFinD -lteBrDl// => /ltW/le_trans; apply.
   by rewrite leeBlDl// leeD.
 suff: mu Ee = 0 by exists Ee.
-have HL_null n : mu (HLf_g_Be n) <= (3%:R / (e / 2))%:E * n.+1%:R^-1%:E.
+have HL_null n : mu (HLf_g_Be n) <= (3 / (e / 2))%:E * n.+1%:R^-1%:E.
   rewrite (le_trans (maximal_inequality _ _ )) ?divr_gt0//.
   rewrite lee_pmul2l ?lte_fin ?divr_gt0//.
   set h := fun x => `|(f_ k \- g_ n) x|%:E * (\1_(B k) x)%:E.

theories/lebesgue_measure.v

@@ -2115,7 +2115,7 @@ Lemma ae_pointwise_almost_uniform
     (f_ : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R):
   (forall n, measurable_fun A (f_ n)) -> measurable_fun A g ->
   measurable A -> mu A < +oo ->
-  {ae mu, (forall x, A x -> f_ ^~ x @\oo --> g x)} ->
+  {ae mu, (forall x, A x -> f_ ^~ x @ \oo --> g x)} ->
   (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
     {uniform A `\` B, f_ @ \oo --> g}].
 Proof.