From f89df729f61600b295a928779704d3c9a34f07bd Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 1 Aug 2024 21:28:42 +0900 Subject: [PATCH] fixes #1248 (`to_set` / `xsection`) (#1249) * fixes #1248 --- CHANGELOG_UNRELEASED.md | 5 ++ classical/classical_sets.v | 6 ++ theories/cantor.v | 19 +++-- theories/ereal.v | 24 +++--- theories/function_spaces.v | 68 ++++++++------- theories/lebesgue_integral.v | 12 +-- theories/lebesgue_measure.v | 2 +- theories/normedtype.v | 11 +-- theories/numfun.v | 7 +- theories/topology.v | 160 +++++++++++++++++++---------------- 10 files changed, 171 insertions(+), 143 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index af62a5f2d..894b37d94 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -110,6 +110,8 @@ `parameterized_integral_left`, `parameterized_integral_cvg_at_left`, `parameterized_integral_continuous` + corollary `continuous_FTC2` +- in `classical_sets.v`: + + lemmas `xsectionP`, `ysectionP` ### Changed @@ -238,6 +240,9 @@ + lemmas `floor0`, `floor1` + lemma `le_floor` (use `Num.Theory.floor_le` instead) +- in `topology.v`, `function_spaces.v`, `normedtype.v`: + + local notation `to_set` + ### Infrastructure ### Misc diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 2afe27710..a505f7399 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -3313,9 +3313,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. diff --git a/theories/cantor.v b/theories/cantor.v index 017e0fb39..7e5420394 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -397,18 +397,18 @@ 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 [|]| | |]. @@ -416,10 +416,10 @@ move=> _; split=> [|A [|]| | |]. 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. diff --git a/theories/ereal.v b/theories/ereal.v index d7fdf10fb..9a0635b77 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1284,7 +1284,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 /= ltr_norml//. @@ -1308,7 +1308,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. @@ -1323,7 +1323,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. @@ -1336,7 +1336,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. @@ -1354,10 +1354,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[]. @@ -1372,13 +1371,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) diff --git a/theories/function_spaces.v b/theories/function_spaces.v index a53f552e9..183b4f9ba 100644 --- a/theories/function_spaces.v +++ b/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. @@ -380,7 +378,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. @@ -530,9 +528,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. @@ -546,9 +544,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. @@ -593,13 +591,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. @@ -654,10 +654,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) : @@ -719,10 +719,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}. @@ -749,9 +751,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 -> @@ -840,13 +842,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 @@ -960,13 +963,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. @@ -980,14 +983,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. @@ -1179,7 +1187,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. @@ -1283,7 +1291,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. @@ -1297,14 +1305,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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0a8b66a1d..96bb9ca88 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6568,12 +6568,12 @@ have locg_B n : locally_integrable [set: R] (g_B n). by rewrite 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 => //. @@ -6607,7 +6607,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) \_ (B k). diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 48b1ab735..f08883ee5 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2306,7 +2306,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. diff --git a/theories/normedtype.v b/theories/normedtype.v index 79849cd5d..af25c6317 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -3521,9 +3521,6 @@ Context (A : set T). 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. - (* 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 @@ -3670,7 +3667,7 @@ exists (Uniform.class urysohnType), (apxU (U, ~` B)); split => //. by have /subset_closure ? := AU _ Aa; case. move=> x ? [E gE] /(@filterS T); apply; move: gE. rewrite /= /ury_unif filterI_iterE; case => K /= [i _] /= uiK KE. -suff : @nbhs T T x to_set K (x) by apply: filterS => y /KE. +suff : @nbhs T T x [set y | K (x, y)] by apply: filterS => y /KE/xsectionP. elim: i K uiK {E KE}; last by move=> ? H ? [N] /H ? [M] /H ? <-; apply: filterI. move=> K [->|]; first exact: filterT. move=> [[/= P Q] [/= oP oQ AP cPQ <-]]; rewrite /apxU /=. @@ -3776,7 +3773,7 @@ rewrite openE => /(_ _ nBx); rewrite /interior /= -nbhs_entourageE. case=> E entE EnB. pose T' := [the pseudoMetricType Rdefinitions.R of gauge.type entE]. exists (Uniform.class T); exists E; split => //; last by move => ?. -by rewrite -subset0 => -[? w [/= [-> ? ?]]]; exact: (EnB w). +by rewrite -subset0 => -[? w [/= [-> ? /xsectionP ?]]]; exact: (EnB w). Qed. Lemma uniform_completely_regular {R : realType} {T : uniformType} : @@ -3795,7 +3792,7 @@ Lemma uniform_regular {X : uniformType} : @regular_space X. Proof. move=> x A; rewrite /= -nbhs_entourageE => -[E entE]. move/(subset_trans (ent_closure entE)) => ExA. -by exists [set y | split_ent E (x, y)]; first by exists (split_ent E). +by exists (xsection (split_ent E) x) => //; exists (split_ent E). Qed. Lemma regular_openP {T : topologicalType} (x : T) : @@ -5700,7 +5697,7 @@ Lemma vitali_lemma_finite (s : seq I) : forall i, i \in s -> exists j, [/\ j \in D, B i `&` B j !=set0, radius (B j) >= radius (B i) & - B i `<=` 3%:R *` B j] ] }. + B i `<=` 3 *` B j] ] }. Proof. pose LE x y := radius (B x) <= radius (B y). have LE_trans : transitive LE by move=> x y z; exact: le_trans. diff --git a/theories/numfun.v b/theories/numfun.v index 5cc723fde..c2399385f 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -555,7 +555,7 @@ have [|?] := pselect (forall x, A x -> `|f x| <= M); last by exists point. by move=> bd pm cf; have [g ?] := tietze_step' pm cf bd; exists g. Qed. -Let onem_twothirds : 1 - 2/3%:R = 1/3%:R :> R. +Let onem_twothirds : 1 - 2/3 = 1/3 :> R. Proof. by apply/eqP; rewrite subr_eq/= -mulrDl nat1r divrr// unitfE. Qed. Lemma continuous_bounded_extension (f : X -> R^o) M : @@ -569,7 +569,7 @@ pose f_ := fix F n := pose g_ n := projT1 (tietze_step (f_ n) (M2d3 n)). have fgE n : f_ n - f_ n.+1 = g_ n by rewrite /= opprB addrC subrK. have twothirds1 : `|2/3| < 1 :> R. - by rewrite gtr0_norm //= ltr_pdivrMr// mul1r ltr_nat. + by rewrite gtr0_norm//= ltr_pdivrMr// mul1r ltr_nat. have f_geo n : {within A, continuous f_ n} /\ (forall x, A x -> `|f_ n x| <= geometric M%:num (2/3) n). elim: n => [|n [ctsN bdN]]; first by split=> //= x ?; rewrite expr0 mulr1 fbd. @@ -581,8 +581,7 @@ have g_cts n : continuous (g_ n). have g_bd n : forall x, `|g_ n x| <= geometric ((1/3) * M%:num) (2/3) n. have [ctsN bdfN] := f_geo n; rewrite /geometric /= -[_ * M%:num * _]mulrA. by have [_ _] := projT2 (tietze_step (f_ n) _) ctsN (MN0 n) bdfN. -pose h_ : nat -> arrow_uniform_type X R^o := - @series {uniform X -> _} g_. +pose h_ : nat -> arrow_uniform_type X R^o := @series {uniform X -> _} g_. have cvgh' : cvg (h_ @ \oo). apply/cauchy_cvgP/cauchy_ballP => eps epos; near_simpl. suff : \forall x & x' \near \oo, (x' <= x)%N -> ball (h_ x) eps (h_ x'). diff --git a/theories/topology.v b/theories/topology.v index fafdc65ba..25686fd45 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -438,7 +438,6 @@ Reserved Notation "x ^'" (at level 2, format "x ^'"). Reserved Notation "{ 'within' A , 'continuous' f }" (at level 70, A at level 69, format "{ 'within' A , 'continuous' f }"). - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3997,14 +3996,11 @@ End totally_disconnected. 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. - Definition nbhs_ {T T'} (ent : set_system (T * T')) (x : T) := - filter_from ent (fun A => to_set A x). + filter_from ent (fun A => xsection A x). Lemma nbhs_E {T T'} (ent : set_system (T * T')) x : - nbhs_ ent x = filter_from ent (fun A => to_set A x). + nbhs_ ent x = filter_from ent (fun A => xsection A x). Proof. by []. Qed. HB.mixin Record Nbhs_isUniform_mixin M of Nbhs M := { @@ -4035,18 +4031,18 @@ HB.builders Context M of Nbhs_isUniform M. Lemma nbhs_filter (p : M) : ProperFilter (nbhs p). Proof. -rewrite nbhsE nbhs_E; apply filter_from_proper; last first. - by move=> A entA; exists p; apply: entourage_refl entA _ _. +rewrite nbhsE nbhs_E; apply: filter_from_proper; last first. + by move=> A entA; exists p; apply/mem_set; apply: entourage_refl entA _ _. apply: filter_from_filter. - by exists setT; apply: @filterT entourage_filter. -move=> A B entA entB; exists (A `&` B) => //. + by exists setT; exact: @filterT entourage_filter. +move=> A B entA entB; exists (A `&` B); last by rewrite xsectionI. exact: (@filterI _ _ entourage_filter). Qed. Lemma nbhs_singleton (p : M) A : nbhs p A -> A p. Proof. rewrite nbhsE nbhs_E => - [B entB sBpA]. -by apply: sBpA; apply: entourage_refl entB _ _. +by apply/sBpA/mem_set; apply: entourage_refl entB _ _. Qed. Lemma nbhs_nbhs (p : M) A : nbhs p A -> nbhs p (nbhs^~ A). @@ -4054,7 +4050,7 @@ Proof. rewrite nbhsE nbhs_E => - [B entB sBpA]. have /entourage_split_ex[C entC sC2B] := entB. exists C => // q Cpq; rewrite nbhs_E; exists C => // r Cqr. -by apply/sBpA/sC2B; exists q. +by apply/sBpA/mem_set/sC2B; exists q; exact/set_mem. Qed. HB.instance Definition _ := Nbhs_isNbhsTopological.Build M @@ -4088,8 +4084,11 @@ Lemma entourage_sym {X Y : Type} E (x : X) (y : Y) : Proof. by []. Qed. Lemma filter_from_entourageE {M : uniformType} x : - filter_from (@entourage M) (fun A => to_set A x) = nbhs x. -Proof. by rewrite -nbhs_entourageE. Qed. + filter_from (@entourage M) (fun A => [set y | A (x, y)]) = nbhs x. +Proof. +rewrite -nbhs_entourageE; congr filter_from. +by apply/funext => A; apply/seteqP; split => y/= /xsectionP. +Qed. Module Export NbhsEntourage. Definition nbhs_simpl := @@ -4149,18 +4148,18 @@ Lemma subset_split_ent (A : set (M * M)) : entourage A -> Proof. by move=> /split_entP []. Qed. Lemma entourage_split (z x y : M) A : entourage A -> - split_ent A (x,z) -> split_ent A (z,y) -> A (x,y). -Proof. by move=> /subset_split_ent sA ??; apply: sA; exists z. Qed. + split_ent A (x, z) -> split_ent A (z, y) -> A (x, y). +Proof. by move=> /subset_split_ent sA ? ?; apply: sA; exists z. Qed. -Lemma nbhs_entourage (x : M) A : entourage A -> nbhs x (to_set A x). +Lemma nbhs_entourage (x : M) A : entourage A -> nbhs x (xsection A x). Proof. by move=> ?; apply/nbhsP; exists A. Qed. Lemma cvg_entourageP F (FF : Filter F) (p : M) : F --> p <-> forall A, entourage A -> \forall q \near F, A (p, q). Proof. by rewrite -filter_fromP !nbhs_simpl. Qed. -Lemma cvg_entourage {F} {FF : Filter F} (y : M) : - F --> y -> forall A, entourage A -> \forall y' \near F, A (y,y'). +Lemma cvg_entourage {F} {FF : Filter F} (x : M) : + F --> x -> forall A, entourage A -> \forall y \near F, A (x, y). Proof. by move/cvg_entourageP. Qed. Lemma cvg_app_entourageP T (f : T -> M) F (FF : Filter F) p : @@ -4187,15 +4186,16 @@ Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core. Hint Extern 0 (entourage (_^-1)%classic) => exact: entourage_inv : core. Arguments entourage_split {M} z {x y A}. #[global] -Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core. +Hint Extern 0 (nbhs _ (xsection _ _)) => exact: nbhs_entourage : core. Lemma ent_closure {M : uniformType} (x : M) E : entourage E -> - closure (to_set (split_ent E) x) `<=` to_set E x. + closure (xsection (split_ent E) x) `<=` xsection E x. Proof. pose E' := (split_ent E) `&` ((split_ent E)^-1)%classic. -move=> entE z /(_ [set y | E' (z, y)])[]. +move=> entE z /(_ (xsection E' z))[]. by rewrite -nbhs_entourageE; exists E' => //; exact: filterI. -by move=> y [/=] + [_]; exact: entourage_split. +move=> y; rewrite xsectionI => -[/xsectionP xy [_ /xsectionP yz]]. +by apply/xsectionP; move: xy yz; exact: entourage_split. Qed. Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x : @@ -4234,7 +4234,7 @@ Section uniform_closeness. Variable (U : uniformType). Lemma open_nbhs_entourage (x : U) (A : set (U * U)) : - entourage A -> open_nbhs x (to_set A x)^°. + entourage A -> open_nbhs x (xsection A x)^°. Proof. move=> entA; split; first exact: open_interior. by apply: nbhs_singleton; apply: nbhs_interior; apply: nbhs_entourage. @@ -4246,10 +4246,12 @@ rewrite propeqE; split=> [cxy A entA|cxy]. have /entourage_split_ent entsA := entA; rewrite closeEnbhs in cxy. have yl := nbhs_entourage _ (entourage_inv entsA). have yr := nbhs_entourage _ entsA. - have [z [zx zy]] := cxy _ _ (yr x) (yl y). + have [z [/xsectionP zx /xsectionP zy]] := cxy _ _ (yr x) (yl y). exact: (entourage_split z). rewrite closeEnbhs => A B /nbhsP[E1 entE1 sE1A] /nbhsP[E2 entE2 sE2B]. -by exists y; split;[apply: sE1A; apply: cxy|apply: sE2B; apply: entourage_refl]. +exists y; split. +- by apply/sE1A/xsectionP; exact: cxy. +- by apply/sE2B/xsectionP; exact: entourage_refl. Qed. Lemma close_trans (y x z : U) : close x y -> close y z -> close x z. @@ -4261,8 +4263,8 @@ Qed. Lemma close_cvgxx (x y : U) : close x y -> x --> y. Proof. rewrite entourage_close => cxy P /= /nbhsP[A entA sAP]. -apply/nbhsP; exists (split_ent A) => // z xz; apply: sAP. -apply: (entourage_split x) => //. +apply/nbhsP; exists (split_ent A) => // z /xsectionP xz; apply: sAP. +apply/xsectionP; apply: (entourage_split x) => //. by have := cxy _ (entourage_inv (entourage_split_ent entA)). Qed. @@ -4348,13 +4350,14 @@ rewrite predeq2E => xy A; split=> [[B []] | [B [C [entC1 entC2] sCB] sBA]]. rewrite -!nbhs_entourageE => - [C1 entC1 sCB1] [C2 entC2 sCB2] sBA. exists [set xy | C1 (xy.1.1, xy.2.1) /\ C2 (xy.1.2, xy.2.2)]. exact: prod_entP. - by move=> uv [/= /sCB1 Buv1 /sCB2 /(conj Buv1) /sBA]. -exists (to_set (C.1) (xy.1), to_set (C.2) (xy.2)). + move=> uv /xsectionP/= [/xsectionP/sCB1 Buv1 /xsectionP/sCB2/(conj Buv1)]. + exact: sBA. +exists (xsection C.1 xy.1, xsection C.2 xy.2). by rewrite -!nbhs_entourageE; split; [exists C.1|exists C.2]. -move=> uv [/= Cxyuv1 Cxyuv2]; apply: sBA. -have /sCB : (C.1 `*` C.2) ((xy.1,uv.1),(xy.2,uv.2)) by []. +move=> uv [/= /xsectionP Cxyuv1 /xsectionP Cxyuv2]; apply: sBA. +have /sCB : (C.1 `*` C.2) ((xy.1,uv.1), (xy.2,uv.2)) => //. move=> [zt Bzt /eqP]; rewrite !xpair_eqE andbACA -!xpair_eqE. -by rewrite /= -!surjective_pairing => /eqP<-. +by rewrite -!surjective_pairing => /eqP ztE; apply/xsectionP; rewrite -ztE. Qed. HB.instance Definition _ := Nbhs_isUniform.Build (U * V)%type @@ -4415,16 +4418,16 @@ Lemma mx_ent_nbhsE : nbhs = nbhs_ mx_ent. Proof. rewrite predeq2E => M A; split. move=> [B]; rewrite -nbhs_entourageE => M_B sBA. - set sB := fun i j => [set C | entourage C /\ to_set C (M i j) `<=` B i j]. + set sB := fun i j => [set C | entourage C /\ xsection C (M i j) `<=` B i j]. have {}M_B : forall i j, sB i j !=set0 by move=> ??; apply/exists2P/M_B. exists [set MN : 'M[T]_(m, n) * 'M[T]_(m, n) | forall i j, get (sB i j) (MN.1 i j, MN.2 i j)]. by exists (fun i j => get (sB i j)) => // i j; have /getPex [] := M_B i j. - move=> N CMN; apply/sBA => i j; have /getPex [_] := M_B i j; apply. - exact/CMN. -move=> [B [C entC sCB] sBA]; exists (fun i j => to_set (C i j) (M i j)). + move=> N /xsectionP CMN; apply/sBA => i j; have /getPex [_] := M_B i j; apply. + exact/xsectionP/CMN. +move=> [B [C entC sCB] sBA]; exists (fun i j => xsection (C i j) (M i j)). by rewrite -nbhs_entourageE => i j; exists (C i j). -by move=> N CMN; apply/sBA/sCB. +by move=> N CMN; apply/sBA; apply/xsectionP/sCB => ? ?; exact/xsectionP/CMN. Qed. HB.instance Definition _ := Nbhs_isUniform.Build 'M[T]_(m, n) @@ -4436,13 +4439,16 @@ Lemma cvg_mx_entourageP (T : uniformType) m n (F : set_system 'M[T]_(m,n)) (FF : Filter F) (M : 'M[T]_(m,n)) : F --> M <-> forall A, entourage A -> \forall N \near F, - forall i j, A (M i j, (N : 'M[T]_(m,n)) i j). + forall i j, (M i j, (N : 'M[T]_(m,n)) i j) \in A. Proof. split. - by rewrite filter_fromP => FM A ?; apply: (FM (fun i j => to_set A (M i j))). -move=> FM; apply/cvg_entourageP => A [P entP sPA]; near=> N. -apply: sPA => /=; near: N; set Q := \bigcap_ij P ij.1 ij.2. -apply: filterS (FM Q _); first by move=> N QN i j; apply: (QN _ _ (i, j)). + rewrite filter_fromP => FM A ?. + by apply: (FM (fun i j => xsection A (M i j))). +move=> FM; apply/cvg_entourageP => A [P entP sPA]; near=> N; apply/xsectionP. +move/subsetP : sPA; apply => /=; near: N; set Q := \bigcap_ij P ij.1 ij.2. +apply: filterS (FM Q _). + move=> N QN; rewrite inE/= => i j. + by have := QN i j; rewrite !inE => /(_ (i, j)); exact. have -> : Q = \bigcap_(ij in [set k | k \in [fset x in predT]%fset]) P ij.1 ij.2. by rewrite predeqE => t; split=> Qt ij _; apply: Qt => //=; rewrite !inE. @@ -4495,10 +4501,10 @@ rewrite predeq2E => x V; split. move=> /nbhsP [W ? WsubB]; exists ((map_pair f) @^-1` W); first by exists W. by move=>??; exact/BsubV/WsubB. case=> W [V' entV' V'subW] /filterS; apply. -have : nbhs (f x) to_set V' (f x) by apply/nbhsP; exists V'. +have : nbhs (f x) (xsection V' (f x)) by apply/nbhsP; exists V'. rewrite (@nbhsE U) => [[O [openU Ofx Osub]]]. (exists (f @^-1` O); repeat split => //); first by exists O => //. -by move=> w ? ; apply: V'subW; exact: Osub. +by move=> w ?; apply/mem_set; apply: V'subW; apply/set_mem; exact: Osub. Qed. HB.instance Definition _ := @Nbhs_isUniform.Build (weak_topology f) (*S nbhs*) @@ -4581,14 +4587,14 @@ rewrite predeq2E => x V; split. suff -> : V = setT by exists setT; apply: filterT; exact: sup_ent_filter. rewrite -subTset => ??; apply: BV; exists (\bigcap_(i in [set` F]) i) => //. by move=> w /Fsup/set_mem; rewrite /sup_subbase I0 bigcup_set0. - have f : forall w, {p : IEnt | w \in F -> to_set ((projT1 p).2) x `<=` w}. + have f : forall w, {p : IEnt | w \in F -> xsection ((projT1 p).2) x `<=` w}. move=> /= v; apply: cid; case (pselect (v \in F)); first last. by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)). move=> /[dup] /Fx vx /Fsup/set_mem [i _]; rewrite openE => /(_ x vx). by move=> /(@nbhsP (TS i)) [w /asboolP ent ?]; exists (exist _ (i, w) ent). exists (\bigcap_(w in [set` F]) (projT1 (projT1 (f w))).2); first last. - move=> v /= Fgw; apply: BV; exists (\bigcap_(i in [set` F]) i) => //. - by move=> w /[dup] ? /Fgw /= /(projT2 (f w)); exact. + move=> v /= /xsectionP Fgw; apply: BV; exists (\bigcap_(i in [set` F]) i) => //. + by move=> w /[dup] ? /Fgw /= /mem_set/(projT2 (f w)); exact. exists (\bigcap_(w in [set` F]) (projT1 (projT1 (f w))).2) => //. exists [fset (fun i => (projT1 (f i))) w | w in F]%fset. by move=> u ?; exact: in_setT. @@ -4599,7 +4605,7 @@ case=> E [D [/= F FsubEnt <-] FsubE EsubV]. have F_nbhs_x: Filter (nbhs x) by typeclasses eauto. apply: (filterS EsubV). pose f : IEnt -> set T := fun w => - @interior (TS (projT1 w).1) (to_set ((projT1 w).2) (x)). + @interior (TS (projT1 w).1) (xsection (projT1 w).2 x). exists (\bigcap_(w in [set` F]) f w); repeat split. - exists [set \bigcap_(w in [set` F]) f w]; last by rewrite bigcup_set1. move=> ? ->; exists [fset f w | w in F]%fset. @@ -4607,7 +4613,8 @@ exists (\bigcap_(w in [set` F]) f w); repeat split. by apply/mem_set; rewrite /f /=; exists i => //; exact: open_interior. by rewrite set_imfset bigcap_image //=. - by IEntP=> ? ? /open_nbhs_entourage entw ??; apply entw. -- by move=> t /= Ifwt; apply: FsubE => it /Ifwt/interior_subset. +- move=> t /= Ifwt. + by apply/mem_set/FsubE => it /Ifwt/interior_subset => /set_mem. Qed. HB.instance Definition _ := @Nbhs_isUniform.Build Tt sup_ent @@ -4796,9 +4803,10 @@ Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : @nbhs_ball R M = nbhs. Proof. rewrite predeq2E => x P; rewrite -nbhs_entourageE; split. - by move=> [_/posnumP[e] sbxeP]; exists [set xy | ball xy.1 e%:num xy.2]. + move=> [_/posnumP[e] sbxeP]; exists [set xy | ball xy.1 e%:num xy.2] => //. + by move=> y /xsectionP/sbxeP. rewrite -entourage_ballE; move=> [A [e egt0 sbeA] sAP]. -by exists e => // ??; apply/sAP/sbeA. +by exists e => // ? ?; exact/sAP/xsectionP/sbeA. Qed. Lemma filter_from_ballE {R : numDomainType} {M : pseudoMetricType R} x : @@ -5199,9 +5207,9 @@ Lemma discrete_pointed (T : pointedType) : discrete_space (pointed_discrete_topology T). Proof. apply/funext => /= x; apply/funext => A; apply/propext; split. -- by move=> [E hE EA] x0 ->{x0}; apply: EA => /=; apply: hE => /=; exists x. +- by move=> [E hE EA] _ ->; apply/EA/xsectionP/hE; exists x. - move=> h; exists [set x | x.1 = x.2]; first by move=> -[a b] [t _] [<- <-]. - by move=> y /= xy; exact: h. + by move=> y /xsectionP/= xy; exact: h. Qed. (** Complete uniform spaces *) @@ -5212,10 +5220,11 @@ Lemma cvg_cauchy {T : uniformType} (F : set_system T) : Filter F -> [cvg F in T] -> cauchy F. Proof. move=> FF cvF A entA; have /entourage_split_ex [B entB sB2A] := entA. -exists (to_set ((B^-1)%classic) (lim F), to_set B (lim F)). +exists (xsection ((B^-1)%classic) (lim F), xsection B (lim F)). split=> /=; apply: cvF; rewrite /= -nbhs_entourageE; last by exists B. by exists (B^-1)%classic => //; apply: entourage_inv. -by move=> ab [/= Balima Blimb]; apply: sB2A; exists (lim F). +move=> ab [/= /xsectionP Balima /xsectionP Blimb]; apply: sB2A. +by exists (lim F). Qed. HB.mixin Record Uniform_isComplete T of Uniform T := { @@ -5255,8 +5264,9 @@ have /(_ _ _) /cauchy_cvg /cvg_app_entourageP cvF : apply/cvg_ex. set Mlim := \matrix_(i, j) (lim ((fun M : 'M[T]_(m, n) => M i j) @ F) : T). exists Mlim; apply/cvg_mx_entourageP => A entA; near=> M => i j; near F => M'. +rewrite inE. apply: subset_split_ent => //; exists (M' i j) => /=. - by near: M'; rewrite mxE; apply: cvF. + by near: M'; rewrite mxE; exact: cvF. move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: Fc. by exists (fun _ _ => (split_ent A)^-1%classic) => ?? //; apply: entourage_inv. Unshelve. all: by end_near. Qed. @@ -5311,7 +5321,6 @@ HB.structure Definition CompletePseudoMetric R := HB.instance Definition _ (R : numFieldType) (T : completePseudoMetricType R) (m n : nat) := Uniform_isComplete.Build 'M[T]_(m, n) cauchy_cvg. - HB.instance Definition _ (R : zmodType) := isPointed.Build R 0. Lemma compact_cauchy_cvg {T : uniformType} (U : set T) (F : set_system T) : @@ -5321,8 +5330,8 @@ move=> PF cf FU /(_ F PF FU) [x [_ clFx]]; apply: (cvgP x). apply/cvg_entourageP => E entE. have : nbhs entourage (split_ent E) by rewrite nbhs_filterE. move=> /(cf (split_ent E))[] [D1 D2]/= /[!nbhs_simpl] -[FD1 FD2 D1D2E]. -have : nbhs x to_set (split_ent E) x by exact: nbhs_entourage. -move=> /(clFx _ (to_set (split_ent E) x) FD1)[z [Dz Exz]]. +have : nbhs x (xsection (split_ent E) x) by exact: nbhs_entourage. +move=> /(clFx _ (xsection (split_ent E) x) FD1)[z [Dz /xsectionP Exz]]. by near=> t; apply/(entourage_split z entE Exz)/D1D2E; split => //; near: t. Unshelve. all: by end_near. Qed. @@ -5382,8 +5391,9 @@ Lemma nbhs_ball_normE : Proof. rewrite /nbhs_ entourage_E predeq2E => x A; split. move=> [e egt0 sbeA]. - by exists [set xy | ball_ Num.norm xy.1 e xy.2] => //; exists e. -by move=> [E [e egt0 sbeE] sEA]; exists e => // ??; apply/sEA/sbeE. + exists [set xy | ball_ Num.norm xy.1 e xy.2]; first by exists e. + by move=> r /xsectionP; exact: sbeA. +by move=> [E [e egt0 sbeE] sEA]; exists e => // ? ?; exact/sEA/xsectionP/sbeE. Qed. End pseudoMetric_of_normedDomain. @@ -6392,20 +6402,20 @@ rewrite funeq2E=> x U. case: (@nbhs_subspaceP X A x); rewrite propeqE; split => //=. - rewrite withinE; case=> V /[dup] nbhsV => [/nbhsP [E entE Esub] UV]. exists [set xy | xy.1 = xy.2 \/ A xy.1 /\ A xy.2 /\ E xy]. - by exists E => //= [[??]] /= [->| [?[]]//]; exact: entourage_refl. - move=> y /= [<-|]. + by exists E => //= [[? ?]] /= [->| [? []]//]; exact: entourage_refl. + move=> y /= /xsectionP/= -[<-{y}|]. suff : (U `&` A) x by case. - by rewrite UV; split => //; apply: (@nbhs_singleton X). + by rewrite UV; split => //; exact: (@nbhs_singleton X). case=> _ [Ay Ey]; suff : (U `&` A) y by case. - by rewrite UV; split => //; apply: Esub. + by rewrite UV; split => //; exact/Esub/xsectionP. - move=> [] W [E eentE subW] subU //=. - near=> w; apply: subU; apply: subW; right; repeat split => //=. - by exact: (near (withinT _ (@nbhs_filter X _))). - by near: w; apply/nbhsP; exists E => // y /= Ey. + near=> w; apply/subU/xsectionP/subW; right; repeat split => //=. + exact: (near (withinT _ (@nbhs_filter X _))). + by near: w; apply/nbhsP; exists E => // y /xsectionP. - move=> //= Ux; exists EA => //. - by move=> y /= [|[]] //= <-; apply: Ux. + by move=> y /xsectionP => -[|[]] //= <-; exact: Ux. - rewrite //= => [[W [W' entW' subW] subU]] ? ->. - by apply: subU; apply: subW; left. + by apply/subU/xsectionP/subW; left. Unshelve. all: by end_near. Qed. HB.instance Definition _ := Nbhs_isUniform_mixin.Build (subspace A) @@ -6663,14 +6673,14 @@ Lemma uniform_regular {T : uniformType} : @regular_space T. Proof. move=> x R /=; rewrite -{1}nbhs_entourageE => -[E entE ER]. pose E' := split_ent E; have eE' : entourage E' by exact: entourage_split_ent. -exists (to_set (E' `&` E'^-1%classic) x). +exists (xsection (E' `&` E'^-1%classic) x). rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. exact: filterI. -move=> z /= clEz; apply: ER; apply: subset_split_ent => //. -have [] := clEz (to_set (E' `&` E'^-1%classic) z). +move=> z /= clEz; apply/ER/xsectionP; apply: subset_split_ent => //. +have [] := clEz (xsection (E' `&` E'^-1%classic) z). rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. exact: filterI. -by move=> y /= [[? ?]] [? ?]; exists y. +by move=> y /= [/xsectionP[? ?] /xsectionP[? ?]]; exists y. Qed. #[global] Hint Resolve uniform_regular : core.