From fb5a2c7780c54ce2477217bfe2369d385fdd7bdf Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 21 Apr 2023 20:15:12 -0400 Subject: [PATCH 01/15] curry of continuous functions --- theories/topology.v | 181 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 181 insertions(+) diff --git a/theories/topology.v b/theories/topology.v index ebfcbd7493..0de493dc0b 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -8207,3 +8207,184 @@ exact: precompact_pointwise_precompact. Qed. End ArzelaAscoli. + +Lemma fst_open {U V : topologicalType} (A : set (U * V)) : + open A -> open (fst @` A). +Proof. +rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [Pa ?] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => //. +move=> p Pp; exists (p, b) => //; apply: pqA; split => //. +exact: nbhs_singleton. +Qed. + +Lemma snd_open {U V : topologicalType} (A : set (U * V)) : + open A -> open (snd @` A). +Proof. +rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [? Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => //. +move=> q Qq; exists (a, q) => //; apply: pqA; split => //. +exact: nbhs_singleton. +Qed. + +Lemma near_powerset_map {T U : topologicalType} (f : T -> U) (F : set (set T)) + (P : (set U) -> Prop) : + ProperFilter F -> + (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> + (\forall y \near powerset_filter_from F, P (f @` y)). +Proof. +move=> FF [] G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from F). + by apply: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. +near=> M; apply: GP; apply: (Gs D) => //. + apply: filterS; first exact: preimage_image. + by apply: (near (near_small_set _) M). +have : M `<=` f @^-1` D by apply: (near (small_set_sub FfD) M). +by move/image_subset/subset_trans; apply; apply: image_preimage_subset. +Unshelve. all: by end_near. Qed. + +Lemma near_map_powerset {T U : topologicalType} (f : T -> U) (F : set (set T)) + (P : (set U) -> Prop) : + (forall X Y, X `<=` Y -> P Y -> P X) -> + ProperFilter F -> + (\forall y \near powerset_filter_from F, P (f @` y)) -> + (\forall y \near powerset_filter_from (f x @[x --> F]), P y). +Proof. +move=> Psub FF [] G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). + by apply: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. +have ffiD : fmap f F (f@` D). + by rewrite /fmap /=; apply: filterS; first exact: preimage_image. +near=> M; have FfM : (fmap f F M) by apply (near (near_small_set _) M). +apply: (@Psub _ (f@`D)); first exact: (near (small_set_sub ffiD) M). +exact: GP. +Unshelve. all: by end_near. Qed. + +Section currying. +Context {U : topologicalType} {V W : uniformType}. + +Hypothesis lcU : locally_compact [set: U]. +Hypothesis hsdf : hausdorff_space U. + +Let UV := [topologicalType of (U * V)]. +Definition curry (f : {family compact, UV -> W}) : + {family compact, U -> [uniformType of {family compact, V -> W}]} := + fun u v => f (u, v). + +Lemma continuous_curry (f : {family compact, UV -> W}) : + continuous f -> continuous (curry f). +Proof. +move=> ctsf x; apply/pointwise_compact_cvg; first last. + apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. + have [[P Q] [Px Qy] PQfE] : nbhs (x, y) (f@^-1` E). + by apply: ctsf; apply: open_nbhs_nbhs. + rewrite nbhs_simpl /=; near=> z; rewrite /curry /=. + by apply: PQfE => /=; split; last exact: nbhs_singleton; apply (near Px z). +have Pfx : ProperFilter (powerset_filter_from (curry f x @[x --> x])). + apply: powerset_filter_from_filter. +have Pfx2 : ProperFilter (powerset_filter_from (nbhs (curry f x))). + apply: powerset_filter_from_filter. +apply: near_map_powerset; first exact: equicontinuous_subset_id. +have [A] := @lcU x I; rewrite withinET => nAx [cptA clA]. +exists [set W | nbhs x W /\ W `<=` A] => /=; first split. +- by move=> ? []. +- by move=> E1 E2 [nE1 E1A E2x ?]; split => //; apply: (subset_trans _ E1A). +- by exists A; split. +move=> B /= [Bx BA] y /= E entE; near=> z => + [ + + <-] => _; near: z. +suff : \forall x0 \near y, forall x1 : U, closure B x1 -> + E (f (x1, y), f (x1, x0)). + by apply: filter_app; apply: nearW=> ? + ? ?; apply; apply/subset_closure. +have /compact_near_coveringP : compact (closure B). + apply: (subclosed_compact _ cptA); first exact: closed_closure. + by rewrite closure_id in clA; rewrite clA; apply: closure_subset. +apply => x' clBx'; near (powerset_filter_from (@entourage W)) => E'. +have entE' : entourage E' by exact: (near (near_small_set _)). +have : nbhs (x' , y) (f@^-1` (to_set E' (f (x',y)))). + by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. +case; case=> P Q /= [Px Qy] PQfE; exists (P, Q); first by split => //. +case=> a b /= [Pa Qb]; apply: subset_split_ent => //. +exists (f (x', y)); last by apply: (near (small_ent_sub _) E')=>//; exact: PQfE. +apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. +by apply: PQfE; split => //; apply: nbhs_singleton. +Unshelve. all: by end_near. Qed. + + + + near_simpl; near=> i j => /=. +apply: PQfE. +exists (P, Q); [by split|]; move => ij /PQfE /=. +have := PQfE (i,j). + exists Q. + Search (nbhs _ (to_set _ _)). +near=> A'. + have : A' `<=` A. + have := (near (small_set_sub nAx) A'). +y E entE. +suff : \forall y' \near y, forall x1, closure B x1 -> (E (f )) +have : \forall C \near powerset_filter_from (nbhs y), forall a, A x -> + (E (a )) + +near=> y' => + [z Az <-] => _. +suff : (fun xy => (f xy.1, f xy.2)) @^-1` E () + +have := ctsf (to_set E (f (x,y))). +move: E entE y; near: A. +have := ctsf + + +suff : \forall W0 \near powerset_filter_from (nbhs (curry f x)), + equicontinuous W0 id. + apply: filter_app. + +near=> E. +have Efx : nbhs (curry f x) E. apply (near (near_small_set Pfx)). + done. +near=> z => g Eg. +have := +have Q := ctsf (x ) (to_set J (g y)). + + + + + + apply: open_nbhs_nbhs; split => //; have : + apply: fst_open; apply: open_comp => //. + congr (open _). rewrite eqEsubset; split => z /=. + case=> [w v <-]. + + + + fst + have -> : [set z | E (curry f z y)] = proj @` + have : nbhs (x,y) (f @^-1` E). + move=> D /=; rewrite nbhsE /=; case => O [oO ocfx] /filterS; apply. + rewrite nbhs_simpl /=. + apply: open_nbhs_nbhs; split => //. + have := curry f @^-1` O = proj x + +apply/uniform_restrict_cvg => E; rewrite /= nbhs_simpl /= nbhs_simpl /=. +suff : {uniform A, curry f x @[x --> x] --> curry f x}. + + + +rewrite /= -nbhs_entourageE; case=> /= E entE /filterS; apply. +move: entE; rewrite /entourage /=. +have := ctsf + +Lemma curry_continuous (f : {family compact, UV -> W}) : + continuous f -> {for f, continuous curry}. +Proof. +move=> ctsf ; apply/ fam_cvgP; first exact/fmap_filter/nbhs_filter. +move=> A cptA. + +apply/uniform_restrict_cvg; first exact/fmap_filter/nbhs_filter. +move=> E /=. +move=> L [/= I []] [N oN <- /= Ncf] /filterS. apply. + apply/fmap_filter/fmap_filter/nbhs_filter. +rewrite nbhs_simpl /= nbhs_simpl /=. + +[/= ? [[/= N oN <-]]] /= Nacf /filterS; apply. + exact/fmap_filter/nbhs_filter. +rewrite /= ?nbhs_simpl /=. + From a5f6fdae96f3f363e292796b266b9a192700222a Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 22 Apr 2023 00:30:57 -0400 Subject: [PATCH 02/15] uncurry continuous, more or less --- theories/topology.v | 131 +++++++++++++++----------------------------- 1 file changed, 43 insertions(+), 88 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 0de493dc0b..a27e2e7d96 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3312,7 +3312,7 @@ Proof. by move=> AsubB [B' B'subB cptB']; exists B' => // ? ?; exact/B'subB/AsubB. Qed. -Lemma compact_precompact (A B : set X) : +Lemma compact_precompact (A : set X) : hausdorff_space X -> compact A -> precompact A. Proof. move=> h c; rewrite precompactE ( _ : closure A = A)//. @@ -8152,7 +8152,7 @@ Qed. Section precompact_equicontinuous. Hypothesis lcptX : locally_compact [set: X]. -Let compact_equicontinuous (W : set {family compact, X -> Y}) : +Lemma compact_equicontinuous (W : set {family compact, X -> Y}) : (forall f, W f -> continuous f) -> compact (W : set {family compact, X -> Y}) -> equicontinuous W id. @@ -8265,15 +8265,14 @@ Section currying. Context {U : topologicalType} {V W : uniformType}. Hypothesis lcU : locally_compact [set: U]. -Hypothesis hsdf : hausdorff_space U. +Hypothesis hsdfU : hausdorff_space U. -Let UV := [topologicalType of (U * V)]. -Definition curry (f : {family compact, UV -> W}) : - {family compact, U -> [uniformType of {family compact, V -> W}]} := - fun u v => f (u, v). +Local Notation "U '~>' V" := + ({family compact, [topologicalType of U] -> [uniformType of V]}) + (at level 99, right associativity). -Lemma continuous_curry (f : {family compact, UV -> W}) : - continuous f -> continuous (curry f). +Lemma continuous_curry (f : U * V ~> W) : + continuous f -> continuous ((curry : ((U * V) ~> W) ~> (U ~> V ~> W)) f). Proof. move=> ctsf x; apply/pointwise_compact_cvg; first last. apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. @@ -8308,83 +8307,39 @@ exists (f (x', y)); last by apply: (near (small_ent_sub _) E')=>//; exact: PQfE. apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. by apply: PQfE; split => //; apply: nbhs_singleton. Unshelve. all: by end_near. Qed. - - - - near_simpl; near=> i j => /=. -apply: PQfE. -exists (P, Q); [by split|]; move => ij /PQfE /=. -have := PQfE (i,j). - exists Q. - Search (nbhs _ (to_set _ _)). -near=> A'. - have : A' `<=` A. - have := (near (small_set_sub nAx) A'). -y E entE. -suff : \forall y' \near y, forall x1, closure B x1 -> (E (f )) -have : \forall C \near powerset_filter_from (nbhs y), forall a, A x -> - (E (a )) - -near=> y' => + [z Az <-] => _. -suff : (fun xy => (f xy.1, f xy.2)) @^-1` E () - -have := ctsf (to_set E (f (x,y))). -move: E entE y; near: A. -have := ctsf - - -suff : \forall W0 \near powerset_filter_from (nbhs (curry f x)), - equicontinuous W0 id. - apply: filter_app. - -near=> E. -have Efx : nbhs (curry f x) E. apply (near (near_small_set Pfx)). - done. -near=> z => g Eg. -have := -have Q := ctsf (x ) (to_set J (g y)). - - - - - - apply: open_nbhs_nbhs; split => //; have : - apply: fst_open; apply: open_comp => //. - congr (open _). rewrite eqEsubset; split => z /=. - case=> [w v <-]. - - - - fst - have -> : [set z | E (curry f z y)] = proj @` - have : nbhs (x,y) (f @^-1` E). - move=> D /=; rewrite nbhsE /=; case => O [oO ocfx] /filterS; apply. - rewrite nbhs_simpl /=. - apply: open_nbhs_nbhs; split => //. - have := curry f @^-1` O = proj x - -apply/uniform_restrict_cvg => E; rewrite /= nbhs_simpl /= nbhs_simpl /=. -suff : {uniform A, curry f x @[x --> x] --> curry f x}. - - - -rewrite /= -nbhs_entourageE; case=> /= E entE /filterS; apply. -move: entE; rewrite /entourage /=. -have := ctsf - -Lemma curry_continuous (f : {family compact, UV -> W}) : - continuous f -> {for f, continuous curry}. -Proof. -move=> ctsf ; apply/ fam_cvgP; first exact/fmap_filter/nbhs_filter. -move=> A cptA. - -apply/uniform_restrict_cvg; first exact/fmap_filter/nbhs_filter. -move=> E /=. -move=> L [/= I []] [N oN <- /= Ncf] /filterS. apply. - apply/fmap_filter/fmap_filter/nbhs_filter. -rewrite nbhs_simpl /= nbhs_simpl /=. - -[/= ? [[/= N oN <-]]] /= Nacf /filterS; apply. - exact/fmap_filter/nbhs_filter. -rewrite /= ?nbhs_simpl /=. +Hypothesis lcV : locally_compact [set: V]. +Hypothesis hsdfV : hausdorff_space V. + +Lemma continuous_snd (f : U ~> V ~> W) v : + continuous f -> continuous (fun q => f q v). +Proof. +move=> ctsf; have [B] := @lcV v I; rewrite withinET; move=> Bu [cptB clB]. +move=> x ?; rewrite /= -nbhs_entourageE; case=> E entE /filterS; apply. +have /ctsf := @fam_nbhs _ _ (@compact V) B _ (f x) entE cptB. +rewrite ?nbhs_simpl /=; apply: filter_app; near=> z => /=. +by apply; apply: nbhs_singleton. +Unshelve. all: by end_near. Qed. + +Lemma continuous_uncurry (f : U ~> V ~> W) : + continuous f -> + (forall u, continuous (f u)) -> + continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). +Proof. +move=> ctsf ctsfp /= [u v] D /=. +rewrite -nbhs_entourageE; case => E entE /filterS; apply. +have [A] := @lcU u I; rewrite withinET; move=> Au [cptA clA]. +have cptfA : compact (f @` A). + by apply: continuous_compact => //; apply: continuous_subspaceT. +have ects : equicontinuous (f @` A) id. + by apply: compact_equicontinuous => //= g [? ? <-]; apply: ctsfp. +near (powerset_filter_from (@entourage W)) => E'. +have entE' : entourage E' by exact: (near (near_small_set _)). +move: (ects) => /(_ v _ entE'); rewrite /prop_near1; set M := (Q in nbhs v Q). +move=> Mv; exists ((fun q => f q v) @^-1` (to_set E' (f u v)) `&` A, M). +split => //; apply: filterI => //; apply: continuous_snd => //=. +case=> a b [/=] [fuav] Aa Mb. +apply: subset_split_ent => //; exists (f a v) => /=; first last. + apply: (near (small_ent_sub _) E') => //; apply: Mb; exists a => //. +apply: (near (small_ent_sub _) E') => //. +Unshelve. all: by end_near. Qed. \ No newline at end of file From dff71f5c6d9f7144c46fedc10f450721a1be119f Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 24 Apr 2023 12:11:00 -0400 Subject: [PATCH 03/15] messy, but fixed assumptions --- theories/topology.v | 293 +++++++++++++++++++++++++++++++++++++++----- 1 file changed, 261 insertions(+), 32 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index a27e2e7d96..85f7ff6d7d 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1649,7 +1649,7 @@ Qed. (* For using near on sets in a filter *) Section NearSet. -Context {T : choiceType} {Y : filteredType T}. +Context {Y : Type}. Context (F : set (set Y)) (PF : ProperFilter F). Definition powerset_filter_from : set (set (set Y)) := filter_from @@ -8085,9 +8085,9 @@ apply: (@entourage_split _ (g y)) => //; first exact: (near (@ectsW x _ _)). by apply/entourage_sym; exact: (near (pointwise_cvg_entourage _ _ _)). Unshelve. all: by end_near. Qed. -Definition small_ent_sub := @small_set_sub _ _ (@entourage Y). +Definition small_ent_sub := @small_set_sub _ (@entourage Y). -Lemma pointwise_compact_cvg (F : set (set {ptws X -> Y})) (f : {ptws X -> Y}) : +Lemma pointwise_compact_cvg (F : set (set (X -> Y))) f : ProperFilter F -> (\forall W \near powerset_filter_from F, equicontinuous W id) -> {ptws, F --> f} <-> {family compact, F --> f}. @@ -8095,13 +8095,15 @@ Proof. move=> PF /near_powerset_filter_fromP; case. exact: equicontinuous_subset_id. move=> W; wlog Wf : f W / W f. - move=> + FW /equicontinuous_closure => /(_ f (closure W)) Q. + move=> + FW /equicontinuous_closure => /(_ f (closure (W : set {ptws X -> Y}))) Q. split => Ff; last by apply: pointwise_cvg_compact_family. - apply Q => //; last by (apply: (filterS _ FW); exact: subset_closure). - by rewrite closureEcvg; exists F; [|split] => // ? /filterS; apply. + apply/Q => //. + by rewrite closureEcvg; exists F; [|split] => // ? /= /filterS; apply. + by apply: (filterS _ FW) => z Wz; apply: subset_closure. move=> FW ectsW; split=> [ptwsF|]; last exact: pointwise_cvg_compact_family. apply/fam_cvgP => K ? U /=; rewrite uniform_nbhs => [[E [eE EsubU]]]. -suff : \forall g \near within W (nbhs f), forall y, K y -> E (f y, g y). +suff : \forall g \near within W (nbhs (f : {ptws X -> Y})), + forall y, K y -> E (f y, g y). rewrite near_withinE; near_simpl => N; apply: (filter_app _ _ FW). by apply: ptwsF; near=> g => ?; apply: EsubU; apply: (near N g). near (powerset_filter_from (@entourage Y)) => E'. @@ -8114,11 +8116,11 @@ apply: (entourage_split (f x) eE). exact: (near (ectsW x E' entE') y). apply: (@entourage_split _ (g x)) => //. apply: (near (small_ent_sub _) E') => //. - near: g; near_simpl; apply: (@cvg_within _ (nbhs f)). + near: g; near_simpl; apply: (@cvg_within _ (nbhs (f : {ptws X -> Y}))). exact: pointwise_cvg_entourage. apply: (near (small_ent_sub _) E') => //. apply: (near (ectsW x E' entE')) => //. -exact: (near (withinT _ (nbhs_filter f))). +exact: (near (withinT _ (nbhs_filter (f : {ptws X -> Y})))). Unshelve. all: end_near. Qed. Lemma pointwise_compact_closure (W : set (X -> Y)) : @@ -8261,29 +8263,133 @@ apply: (@Psub _ (f@`D)); first exact: (near (small_set_sub ffiD) M). exact: GP. Unshelve. all: by end_near. Qed. -Section currying. -Context {U : topologicalType} {V W : uniformType}. +Lemma continuous_fst_arg {U V W : topologicalType} (f : U * V -> W) (u : U) : + continuous f -> continuous (curry f u). +Proof. +move=> ctsf; rewrite (_ : curry f u = f \o (pair u)); last exact:funext. +move=> y; apply: continuous_comp; last exact: ctsf. +by apply: cvg_pair; [exact: cvg_cst | exact: cvg_id]. +Qed. -Hypothesis lcU : locally_compact [set: U]. -Hypothesis hsdfU : hausdorff_space U. +Lemma continuous_snd_arg {U V W : topologicalType} (f : U * V -> W) (v : V) : + continuous f -> continuous (fun q => curry f q v). +Proof. +move=> ctsf; suff : continuous (f \o (fun q => pair q v)) by exact. +move=> y; apply: continuous_comp; last exact: ctsf. +by apply: cvg_pair; [exact: cvg_id | exact: cvg_cst]. +Qed. + +Section currying_pt1. +Context {U V W : uniformType}. Local Notation "U '~>' V" := ({family compact, [topologicalType of U] -> [uniformType of V]}) (at level 99, right associativity). + +Lemma continuous_snd (f : U ~> V ~> W) v : + continuous f -> + (forall u, continuous (f u)) -> + continuous (fun q => f q v). +Proof. +move=> ctsf ctsfp x ?. +rewrite /= -nbhs_entourageE; case=> E entE /filterS; apply. +rewrite ?nbhs_simpl /=; near=> z => /=; near: z. +near (powerset_filter_from (@entourage W)) => E'. +have entE' : entourage E' by exact: (near (near_small_set _)). +have nvE' : nbhs v (f x @^-1` (to_set E' (f x v))). + by apply: ctsfp; rewrite /= -nbhs_entourageE; exists E'. +suff [O Ofx OE] : exists2 O, nbhs (f x) O & (forall g, O g -> E (f x v, g v)). + move/ctsf: Ofx; rewrite /= nbhs_simpl /=; apply: filter_app. + by near_simpl; near=> z => foz; apply: OE. +exists [set g | forall z, [set v] z -> E (f x z, g z)]. + by apply: fam_nbhs => //; exact: compact_set1. +by move=> g; apply. +Unshelve. all: by end_near. Qed. Lemma continuous_curry (f : U * V ~> W) : - continuous f -> continuous ((curry : ((U * V) ~> W) ~> (U ~> V ~> W)) f). + continuous f -> continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)) f). Proof. -move=> ctsf x; apply/pointwise_compact_cvg; first last. +move=> ctsf x; apply/cvg_sup; case => K cptK /=. +have Pfx : ProperFilter (powerset_filter_from (curry f x @[x --> x])). + apply: powerset_filter_from_filter. +have Pfx2 : ProperFilter (powerset_filter_from (nbhs (curry f x))). + apply: powerset_filter_from_filter. +move=> T /= [? [[? oR <- /= Rxcf RT]]]. +move: oR; rewrite openE => /(_ _ Rxcf); case => ? [E entE] EE' EKR. +near=> z; apply/RT/EKR/EE'; case=> w Kiw; have Kw : K w by rewrite inE in Kiw. +rewrite /= /set_val /= /eqincl /incl; move: w Kw {Kiw}; near: z. +rewrite nbhs_simpl; near_simpl; move/compact_near_coveringP : cptK; apply. +move=> v Kv /=. +near (powerset_filter_from (@entourage W)) => E'. +have entE' : entourage E' by exact: (near (near_small_set _)). +have : nbhs (x,v) (f @^-1` to_set E' (f (x,v))). + by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. +case; case=> /= P Q [Px Qy] PQfE. +exists (Q,P); first by split => //. +case=> b a [/=] Qb Pa; rewrite /curry; apply: subset_split_ent => //. +exists (f (x,v)); last by apply: (near (small_ent_sub _) E') => //; apply: PQfE. +rewrite /fst. +apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. +apply: PQfE; split => //; exact: nbhs_singleton. +Unshelve. all: by end_near. Qed. + +exists (setT , curry f x @^-1` [set g | forall (z:V), K z -> E (curry f x z, g z)]). +have /filterS := @fam_nbhs _ W _ K _ (curry f x) entE cptK; apply. +near: z. +apply: (filterS RT); near=> z => /=. +move=> z /= zke; apply/RT/EKR/EE'; case=> w Kw; have ? : K w by rewrite inE in Kw. +exact: zke. +set F := fmap _ _. +have [] := @pointwise_compact_cvg V W F (curry f x) _. + rewrite /F; apply: near_map_powerset; first exact: equicontinuous_subset_id. + admit. +have Pfc : {ptws, F --> curry f x}. + apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. + have [[P Q] [Px Qy] PQfE] : nbhs (x, y) (f@^-1` E). + by apply: ctsf; apply: open_nbhs_nbhs. + rewrite nbhs_simpl /= /F /=. + near=> z; rewrite /curry /=; apply: PQfE => /=. + by split; last exact: nbhs_singleton; apply (near Px z). +move=> /(_ Pfc) + _ => /cvg_trans; apply. +move=> T /= [? [[R oR <- /= Rxcf RT]]]. +move: oR; rewrite openE => /(_ _ Rxcf); case => E' [E entE] EE' EKR. +have /filterS := @fam_nbhs _ W _ K _ (curry f x) entE cptK; apply. +move=> z /= zke; apply/RT/EKR/EE'; case=> w Kw; have ? : K w by rewrite inE in Kw. +exact: zke. +Qed. + +move oR; rewrite -nbhs_entourageE. +rewrite /filter_of /= nbhs_simpl . +congr (cvg_to _); rewrite /filter_of. +move=> R /= [] /= E [[/= J oJ]] <- /= jsgl /filterS; apply. +rewrite nbhs_simpl /=; near=> z => /=; near: z; near_simpl. + + +=> NR. +near=> z => /=. +near=> R. +rewrite +apply/cvg_sup. + admit. +move=> /(_ Pfc) + _. +rewrite /cvg_to /= /GRing.regular. +rewrite /filter_of /= ?nbhs_simpl /nbhs /fct_UniformFamilyFilteredType /=. +rewrite /filter_of /=. +rewrite /nbhs /=. +congr(_ _). +rewrite eqEsubset; split => Z /=. +suff : @nbhs {family compact, V -> W} (curry f x) = nbhs (curry f x : {ptws V -> W}) . + +rewrite eqEsubset; split => R /=; rewrite /nbhs /=. + +simpl. +apply P1. +apply/Q. apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. have [[P Q] [Px Qy] PQfE] : nbhs (x, y) (f@^-1` E). by apply: ctsf; apply: open_nbhs_nbhs. rewrite nbhs_simpl /=; near=> z; rewrite /curry /=. by apply: PQfE => /=; split; last exact: nbhs_singleton; apply (near Px z). -have Pfx : ProperFilter (powerset_filter_from (curry f x @[x --> x])). - apply: powerset_filter_from_filter. -have Pfx2 : ProperFilter (powerset_filter_from (nbhs (curry f x))). - apply: powerset_filter_from_filter. apply: near_map_powerset; first exact: equicontinuous_subset_id. have [A] := @lcU x I; rewrite withinET => nAx [cptA clA]. exists [set W | nbhs x W /\ W `<=` A] => /=; first split. @@ -8308,20 +8414,27 @@ apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. by apply: PQfE; split => //; apply: nbhs_singleton. Unshelve. all: by end_near. Qed. -Hypothesis lcV : locally_compact [set: V]. -Hypothesis hsdfV : hausdorff_space V. - -Lemma continuous_snd (f : U ~> V ~> W) v : - continuous f -> continuous (fun q => f q v). +Lemma continuous_snd (f : U ~> V ~> W) v : + continuous f -> + (forall u, continuous (f u)) -> + continuous (fun q => f q v). Proof. -move=> ctsf; have [B] := @lcV v I; rewrite withinET; move=> Bu [cptB clB]. -move=> x ?; rewrite /= -nbhs_entourageE; case=> E entE /filterS; apply. -have /ctsf := @fam_nbhs _ _ (@compact V) B _ (f x) entE cptB. -rewrite ?nbhs_simpl /=; apply: filter_app; near=> z => /=. -by apply; apply: nbhs_singleton. +move=> ctsf ctsfp x ?. +rewrite /= -nbhs_entourageE; case=> E entE /filterS; apply. +rewrite ?nbhs_simpl /=; near=> z => /=; near: z. +near (powerset_filter_from (@entourage W)) => E'. +have entE' : entourage E' by exact: (near (near_small_set _)). +have nvE' : nbhs v (f x @^-1` (to_set E' (f x v))). + by apply: ctsfp; rewrite /= -nbhs_entourageE; exists E'. +suff [O Ofx OE] : exists2 O, nbhs (f x) O & (forall g, O g -> E (f x v, g v)). + move/ctsf: Ofx; rewrite /= nbhs_simpl /=; apply: filter_app. + by near_simpl; near=> z => foz; apply: OE. +exists [set g | forall z, [set v] z -> E (f x z, g z)]. + by apply: fam_nbhs => //; exact: compact_set1. +by move=> g; apply. Unshelve. all: by end_near. Qed. -Lemma continuous_uncurry (f : U ~> V ~> W) : +Lemma continuous_uncurry (f : U ~> V ~> W): continuous f -> (forall u, continuous (f u)) -> continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). @@ -8331,15 +8444,131 @@ rewrite -nbhs_entourageE; case => E entE /filterS; apply. have [A] := @lcU u I; rewrite withinET; move=> Au [cptA clA]. have cptfA : compact (f @` A). by apply: continuous_compact => //; apply: continuous_subspaceT. +(* have ects : equicontinuous (f @` A) id. by apply: compact_equicontinuous => //= g [? ? <-]; apply: ctsfp. +*) near (powerset_filter_from (@entourage W)) => E'. have entE' : entourage E' by exact: (near (near_small_set _)). -move: (ects) => /(_ v _ entE'); rewrite /prop_near1; set M := (Q in nbhs v Q). +simpl. move=> Mv; exists ((fun q => f q v) @^-1` (to_set E' (f u v)) `&` A, M). split => //; apply: filterI => //; apply: continuous_snd => //=. case=> a b [/=] [fuav] Aa Mb. apply: subset_split_ent => //; exists (f a v) => /=; first last. apply: (near (small_ent_sub _) E') => //; apply: Mb; exists a => //. apply: (near (small_ent_sub _) E') => //. -Unshelve. all: by end_near. Qed. \ No newline at end of file +Unshelve. all: by end_near. Qed. + +End currying_pt1. +Section currying_pt2. +Context {U V : uniformType}. + +Local Notation "U '~>' V" := + ({family compact, [topologicalType of U] -> [uniformType of V]}) + (at level 99, right associativity). + +Hypothesis lcU : locally_compact [set: U]. +Hypothesis hsdfU : hausdorff_space U. + +Definition eval : ((U ~> V) * U) ~> V := fun fx => fx.1 fx.2. + +Lemma eval_continuous (f : U ~> V) (x : U) : + continuous f -> {for (f,x), continuous eval}. +Proof. +move=> ctsf. +have : eval = curry +apply: curry_continuous. +apply: uncurry + + +Lemma curry_continuous (f : ((U * V) ~> W)) : + continuous f -> + (\forall g \near f, continuous (g : U * V ~> W)) -> + {for f, continuous (curry : ((U * V) ~> W) -> (U ~> V ~> W))}. +Proof. +move=> ctsf fgcts. +have ? : ProperFilter (nbhs f). + exact/(@nbhs_pfilter ([topologicalType of (U*V ~> W)]) f). +have ? : ProperFilter (@curry U V [uniformType of W] x @[x-->f]). + exact/fmap_proper_filter. +apply/pointwise_compact_cvg; first last. + apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. + have : nbhs (curry f y : V ~> W) E by apply: open_nbhs_nbhs. + rewrite -nbhs_entourageE /=; case=> N /= entN nfe. + have [A] := @lcU y I; rewrite withinET; move=> Au [cptA clA]. + have cfN := @fam_nbhs _ [uniformType of (V ~> W)] _ A _ (curry f) entN cptA. + rewrite nbhs_simpl /=; near_simpl; near=> z; apply: nfe => /=; near: z. + near_simpl. + suff : nbhs (f : U * V ~> W) [set g : U * V ~> W | E (g \o (pair y))] by apply. + suff : nbhs (f : U * V ~> W) [set g : U * V ~> W | E (g \o (pair y))] by apply. + simpl in *. + apply Q. + have nyE : nbhs y (curry f @^-1` E). + by apply: continuous_curry => //; apply: open_nbhs_nbhs; split. + rewrite ( _ : f = (uncurry (curry f) : U*V ~> W)); first last. + by apply: funext; case=>??; rewrite /curry/uncurry. + have := @continuous_uncurry (curry f) (@continuous_curry f ctsf). + apply: . + Search curry. + suff : nbhs (uncurry (curry f) : U * V ~> W) [set g : U ~> V ~> W | E (g y)]. + suff : + suff -> : [set g : U * V ~> W | | E (g \o pair y)] = (pair) ^-1` E by apply. + + rewrite -nbhs_entourageE /=; case=> N /= entN nfe. + near: z; near_simpl. + rewrite /prop_near1 /=. + continuous_curry. + apply. + move: E oE ecfxy. + + case. + apply. + apply. + + suff : nbhs (f : U * V ~> W) [set g | E (curry g y)] by apply. + suff : continuous (fun (g : U * V ~> W) => (curry g y : V ~> W)). + by apply; apply: open_nbhs_nbhs ; split. + move=> /= g. + suff : [set g | E (curry g y)] `<=` @^-1` E. + move/filterS. + fun w => + (curry f @^-1` E) + rewrite /prop_near1 /= ?nbhs_simpl /=. + pose R := curry f @^-1` E. + have [A] := @lcU y I; rewrite withinET; move=> Au [cptA clA]. + have -> : curry f @^-1` E `<=` (fun g => E (curry g y)). + apply fam_nbhs. + have := @fam_nbhs _ _ (@compact U) A _ (f y) _ cptA. + by apply: open_comp => // + _; apply: continuous_curry. + + near: zhave := . + apply: open_nbhs_nbhs; split => //. + apply: con + have [[P Q] [Px Qy] PQfE] : nbhs (x, y) (f@^-1` E). + by apply: ctsf; apply: open_nbhs_nbhs. + rewrite nbhs_simpl /=; near=> z; rewrite /curry /=. + by apply: PQfE => /=; split; last exact: nbhs_singleton; apply (near Px z). + + apply: near_map_powerset; first exact: equicontinuous_subset_id. + rewrite -(_ : nbhs f = nbhs_of_open _ _) //; near=> K. + move=> /= x E entE; near=> z => + [+ +] <- => _; near: z. + have : nbhs (curry f x : V ~> W) (to_set E (curry f x)). + rewrite -nbhs_entourageE; exists E => //. + have := @continuous_curry _ (ctsf) x (to_set E (curry f x)). + move=>/[apply]; rewrite /= nbhs_simpl /= => nR. + have [A] := @lcU x I; rewrite withinET; move=> Ax [cptA clA]. + near_simpl; near=> z => g Kg. + have : curry f @^-1` to-set E (curry f x). + have := (near nR z) => //. + have := near + + exists ((curry f @^-1` to_set E (curry f x)) `&` A). + case. + apply. + + have := + + + + + From a9281340bc77d98f1b3897dc5dca6f2a644a8dd5 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 24 Apr 2023 13:55:59 -0400 Subject: [PATCH 04/15] uncurry with correct assumptions --- theories/topology.v | 151 ++++---------------------------------------- 1 file changed, 13 insertions(+), 138 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 85f7ff6d7d..42fd05bf7f 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -8333,154 +8333,29 @@ apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. apply: PQfE; split => //; exact: nbhs_singleton. Unshelve. all: by end_near. Qed. -exists (setT , curry f x @^-1` [set g | forall (z:V), K z -> E (curry f x z, g z)]). -have /filterS := @fam_nbhs _ W _ K _ (curry f x) entE cptK; apply. -near: z. -apply: (filterS RT); near=> z => /=. -move=> z /= zke; apply/RT/EKR/EE'; case=> w Kw; have ? : K w by rewrite inE in Kw. -exact: zke. -set F := fmap _ _. -have [] := @pointwise_compact_cvg V W F (curry f x) _. - rewrite /F; apply: near_map_powerset; first exact: equicontinuous_subset_id. - admit. -have Pfc : {ptws, F --> curry f x}. - apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. - have [[P Q] [Px Qy] PQfE] : nbhs (x, y) (f@^-1` E). - by apply: ctsf; apply: open_nbhs_nbhs. - rewrite nbhs_simpl /= /F /=. - near=> z; rewrite /curry /=; apply: PQfE => /=. - by split; last exact: nbhs_singleton; apply (near Px z). -move=> /(_ Pfc) + _ => /cvg_trans; apply. -move=> T /= [? [[R oR <- /= Rxcf RT]]]. -move: oR; rewrite openE => /(_ _ Rxcf); case => E' [E entE] EE' EKR. -have /filterS := @fam_nbhs _ W _ K _ (curry f x) entE cptK; apply. -move=> z /= zke; apply/RT/EKR/EE'; case=> w Kw; have ? : K w by rewrite inE in Kw. -exact: zke. -Qed. - -move oR; rewrite -nbhs_entourageE. -rewrite /filter_of /= nbhs_simpl . -congr (cvg_to _); rewrite /filter_of. -move=> R /= [] /= E [[/= J oJ]] <- /= jsgl /filterS; apply. -rewrite nbhs_simpl /=; near=> z => /=; near: z; near_simpl. - - -=> NR. -near=> z => /=. -near=> R. -rewrite -apply/cvg_sup. - admit. -move=> /(_ Pfc) + _. -rewrite /cvg_to /= /GRing.regular. -rewrite /filter_of /= ?nbhs_simpl /nbhs /fct_UniformFamilyFilteredType /=. -rewrite /filter_of /=. -rewrite /nbhs /=. -congr(_ _). -rewrite eqEsubset; split => Z /=. -suff : @nbhs {family compact, V -> W} (curry f x) = nbhs (curry f x : {ptws V -> W}) . - -rewrite eqEsubset; split => R /=; rewrite /nbhs /=. - -simpl. -apply P1. -apply/Q. - apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. - have [[P Q] [Px Qy] PQfE] : nbhs (x, y) (f@^-1` E). - by apply: ctsf; apply: open_nbhs_nbhs. - rewrite nbhs_simpl /=; near=> z; rewrite /curry /=. - by apply: PQfE => /=; split; last exact: nbhs_singleton; apply (near Px z). -apply: near_map_powerset; first exact: equicontinuous_subset_id. -have [A] := @lcU x I; rewrite withinET => nAx [cptA clA]. -exists [set W | nbhs x W /\ W `<=` A] => /=; first split. -- by move=> ? []. -- by move=> E1 E2 [nE1 E1A E2x ?]; split => //; apply: (subset_trans _ E1A). -- by exists A; split. -move=> B /= [Bx BA] y /= E entE; near=> z => + [ + + <-] => _; near: z. -suff : \forall x0 \near y, forall x1 : U, closure B x1 -> - E (f (x1, y), f (x1, x0)). - by apply: filter_app; apply: nearW=> ? + ? ?; apply; apply/subset_closure. -have /compact_near_coveringP : compact (closure B). - apply: (subclosed_compact _ cptA); first exact: closed_closure. - by rewrite closure_id in clA; rewrite clA; apply: closure_subset. -apply => x' clBx'; near (powerset_filter_from (@entourage W)) => E'. -have entE' : entourage E' by exact: (near (near_small_set _)). -have : nbhs (x' , y) (f@^-1` (to_set E' (f (x',y)))). - by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. -case; case=> P Q /= [Px Qy] PQfE; exists (P, Q); first by split => //. -case=> a b /= [Pa Qb]; apply: subset_split_ent => //. -exists (f (x', y)); last by apply: (near (small_ent_sub _) E')=>//; exact: PQfE. -apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. -by apply: PQfE; split => //; apply: nbhs_singleton. -Unshelve. all: by end_near. Qed. - -Lemma continuous_snd (f : U ~> V ~> W) v : - continuous f -> - (forall u, continuous (f u)) -> - continuous (fun q => f q v). -Proof. -move=> ctsf ctsfp x ?. -rewrite /= -nbhs_entourageE; case=> E entE /filterS; apply. -rewrite ?nbhs_simpl /=; near=> z => /=; near: z. -near (powerset_filter_from (@entourage W)) => E'. -have entE' : entourage E' by exact: (near (near_small_set _)). -have nvE' : nbhs v (f x @^-1` (to_set E' (f x v))). - by apply: ctsfp; rewrite /= -nbhs_entourageE; exists E'. -suff [O Ofx OE] : exists2 O, nbhs (f x) O & (forall g, O g -> E (f x v, g v)). - move/ctsf: Ofx; rewrite /= nbhs_simpl /=; apply: filter_app. - by near_simpl; near=> z => foz; apply: OE. -exists [set g | forall z, [set v] z -> E (f x z, g z)]. - by apply: fam_nbhs => //; exact: compact_set1. -by move=> g; apply. -Unshelve. all: by end_near. Qed. - Lemma continuous_uncurry (f : U ~> V ~> W): + locally_compact [set: V] -> continuous f -> (forall u, continuous (f u)) -> continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). Proof. -move=> ctsf ctsfp /= [u v] D /=. -rewrite -nbhs_entourageE; case => E entE /filterS; apply. -have [A] := @lcU u I; rewrite withinET; move=> Au [cptA clA]. -have cptfA : compact (f @` A). - by apply: continuous_compact => //; apply: continuous_subspaceT. -(* -have ects : equicontinuous (f @` A) id. - by apply: compact_equicontinuous => //= g [? ? <-]; apply: ctsfp. -*) +move=> lcV ctsf ctsfp /= [u v] D /=; rewrite -nbhs_entourageE. +case => E entE /filterS; apply. +have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. near (powerset_filter_from (@entourage W)) => E'. have entE' : entourage E' by exact: (near (near_small_set _)). -simpl. -move=> Mv; exists ((fun q => f q v) @^-1` (to_set E' (f u v)) `&` A, M). -split => //; apply: filterI => //; apply: continuous_snd => //=. -case=> a b [/=] [fuav] Aa Mb. -apply: subset_split_ent => //; exists (f a v) => /=; first last. +have /ctsf /= cfN := @fam_nbhs _ _ _ B _ (f u : V ~> W) entE' cptB. +exists ( + f@^-1`[set g | forall y, B y -> E' (f u y, g y)], + f u @^-1` (to_set E' (f u v)) `&` B). + split => //; apply: filterI => //; apply: ctsfp. + by rewrite /= -nbhs_entourageE /=; exists E'. +case=> a b /= [Eua [Evb Bb]]. +apply: subset_split_ent => //; exists (f u b) => /=. apply: (near (small_ent_sub _) E') => //; apply: Mb; exists a => //. -apply: (near (small_ent_sub _) E') => //. +by apply: (near (small_ent_sub _) E') => //; apply: Eua. Unshelve. all: by end_near. Qed. -End currying_pt1. -Section currying_pt2. -Context {U V : uniformType}. - -Local Notation "U '~>' V" := - ({family compact, [topologicalType of U] -> [uniformType of V]}) - (at level 99, right associativity). - -Hypothesis lcU : locally_compact [set: U]. -Hypothesis hsdfU : hausdorff_space U. - -Definition eval : ((U ~> V) * U) ~> V := fun fx => fx.1 fx.2. - -Lemma eval_continuous (f : U ~> V) (x : U) : - continuous f -> {for (f,x), continuous eval}. -Proof. -move=> ctsf. -have : eval = curry -apply: curry_continuous. -apply: uncurry - - Lemma curry_continuous (f : ((U * V) ~> W)) : continuous f -> (\forall g \near f, continuous (g : U * V ~> W)) -> From 14a892bd991cdb02c0273f1a85904418a2a2ced3 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 24 Apr 2023 21:01:28 -0400 Subject: [PATCH 05/15] curry continuous --- theories/topology.v | 182 ++++++++++++++++++++++---------------------- 1 file changed, 90 insertions(+), 92 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 42fd05bf7f..84e63a2dac 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -8279,12 +8279,63 @@ move=> y; apply: continuous_comp; last exact: ctsf. by apply: cvg_pair; [exact: cvg_id | exact: cvg_cst]. Qed. -Section currying_pt1. -Context {U V W : uniformType}. +Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) : + compact P -> compact Q -> compact (P `*` Q). +Proof. +rewrite ?compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. +have := cptP I F (fun i u => forall q, Q q -> Pr i (u,q)) Ff. +set R := (R in (R -> _) -> _); suff R' : R. + by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. +rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)). +move=> v Qv. +case: (cvfPQ (x,v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. +exists (N2,(N1`*`G)); first by split => //; exists (N1, G) => //. +case=> a [b i] /= [? [?]] ?. +by apply: (ngPr (b,a, i)); split => //; apply: N1N2N. +Unshelve. all: by end_near. Qed. + +Definition near_covering_within {X : topologicalType} (K : set X) := + forall (I : Type) (F : set (set I)) (P : I -> X -> Prop), + Filter F -> + (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> + \near F, K `<=` P F. + +Lemma near_covering_withinP {X : topologicalType} (K : set X): + near_covering_within K <-> near_covering K. +Proof. +split. + move=> cvrW I F P FF cvr. + near=> i; suff : K `<=` (fun q : X => K q -> P i q). + by move=> KKP k Kk; apply: KKP. + near: i; apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app. + by near=> j => /=. +move=> cvrW I F P FF cvr. +near=> i; suff : K `<=` (fun q : X => K q -> P i q). + by move=> KKP k Kk; apply: KKP. +near: i. +have := (cvrW I F (fun i q => K q -> P i q) FF). +apply => x Kx; have := cvr x Kx; apply: filter_app. +by near=> j => + ?; apply. +Unshelve. all: by end_near. Qed. + +Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) + (F : set (set T)) (P : set T) : + Filter F -> (forall i, i \in D -> F ([set j | P j -> f i j])) -> + F ([set j | P j -> (\bigcap_(i in [set i | i \in D]) f i) j]). +Proof. +move=> FF FfD. +have := @filter_bigI T I D f (within P F) (within_filter P FF). +exact. +Qed. + +Section currying. Local Notation "U '~>' V" := ({family compact, [topologicalType of U] -> [uniformType of V]}) - (at level 99, right associativity). + (at level 99, right associativity). + +Section currying_pt1. +Context {U V W : uniformType}. Lemma continuous_snd (f : U ~> V ~> W) v : continuous f -> @@ -8356,94 +8407,41 @@ apply: subset_split_ent => //; exists (f u b) => /=. by apply: (near (small_ent_sub _) E') => //; apply: Eua. Unshelve. all: by end_near. Qed. -Lemma curry_continuous (f : ((U * V) ~> W)) : - continuous f -> - (\forall g \near f, continuous (g : U * V ~> W)) -> - {for f, continuous (curry : ((U * V) ~> W) -> (U ~> V ~> W))}. -Proof. -move=> ctsf fgcts. -have ? : ProperFilter (nbhs f). - exact/(@nbhs_pfilter ([topologicalType of (U*V ~> W)]) f). -have ? : ProperFilter (@curry U V [uniformType of W] x @[x-->f]). - exact/fmap_proper_filter. -apply/pointwise_compact_cvg; first last. - apply/cvg_sup => y D [/= ? [[E oE] <- /=] ecfxy /filterS]; apply. - have : nbhs (curry f y : V ~> W) E by apply: open_nbhs_nbhs. - rewrite -nbhs_entourageE /=; case=> N /= entN nfe. - have [A] := @lcU y I; rewrite withinET; move=> Au [cptA clA]. - have cfN := @fam_nbhs _ [uniformType of (V ~> W)] _ A _ (curry f) entN cptA. - rewrite nbhs_simpl /=; near_simpl; near=> z; apply: nfe => /=; near: z. - near_simpl. - suff : nbhs (f : U * V ~> W) [set g : U * V ~> W | E (g \o (pair y))] by apply. - suff : nbhs (f : U * V ~> W) [set g : U * V ~> W | E (g \o (pair y))] by apply. - simpl in *. - apply Q. - have nyE : nbhs y (curry f @^-1` E). - by apply: continuous_curry => //; apply: open_nbhs_nbhs; split. - rewrite ( _ : f = (uncurry (curry f) : U*V ~> W)); first last. - by apply: funext; case=>??; rewrite /curry/uncurry. - have := @continuous_uncurry (curry f) (@continuous_curry f ctsf). - apply: . - Search curry. - suff : nbhs (uncurry (curry f) : U * V ~> W) [set g : U ~> V ~> W | E (g y)]. - suff : - suff -> : [set g : U * V ~> W | | E (g \o pair y)] = (pair) ^-1` E by apply. - - rewrite -nbhs_entourageE /=; case=> N /= entN nfe. - near: z; near_simpl. - rewrite /prop_near1 /=. - continuous_curry. - apply. - move: E oE ecfxy. - - case. - apply. - apply. - - suff : nbhs (f : U * V ~> W) [set g | E (curry g y)] by apply. - suff : continuous (fun (g : U * V ~> W) => (curry g y : V ~> W)). - by apply; apply: open_nbhs_nbhs ; split. - move=> /= g. - suff : [set g | E (curry g y)] `<=` @^-1` E. - move/filterS. - fun w => - (curry f @^-1` E) - rewrite /prop_near1 /= ?nbhs_simpl /=. - pose R := curry f @^-1` E. - have [A] := @lcU y I; rewrite withinET; move=> Au [cptA clA]. - have -> : curry f @^-1` E `<=` (fun g => E (curry g y)). - apply fam_nbhs. - have := @fam_nbhs _ _ (@compact U) A _ (f y) _ cptA. - by apply: open_comp => // + _; apply: continuous_curry. - - near: zhave := . - apply: open_nbhs_nbhs; split => //. - apply: con - have [[P Q] [Px Qy] PQfE] : nbhs (x, y) (f@^-1` E). - by apply: ctsf; apply: open_nbhs_nbhs. - rewrite nbhs_simpl /=; near=> z; rewrite /curry /=. - by apply: PQfE => /=; split; last exact: nbhs_singleton; apply (near Px z). - - apply: near_map_powerset; first exact: equicontinuous_subset_id. - rewrite -(_ : nbhs f = nbhs_of_open _ _) //; near=> K. - move=> /= x E entE; near=> z => + [+ +] <- => _; near: z. - have : nbhs (curry f x : V ~> W) (to_set E (curry f x)). - rewrite -nbhs_entourageE; exists E => //. - have := @continuous_curry _ (ctsf) x (to_set E (curry f x)). - move=>/[apply]; rewrite /= nbhs_simpl /= => nR. - have [A] := @lcU x I; rewrite withinET; move=> Ax [cptA clA]. - near_simpl; near=> z => g Kg. - have : curry f @^-1` to-set E (curry f x). - have := (near nR z) => //. - have := near - - exists ((curry f @^-1` to_set E (curry f x)) `&` A). - case. - apply. - - have := - - - +Lemma curry_continuous (f : U * V ~> W) : + continuous f -> + {for f, continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)))}. +Proof. +move=> ctsf; apply/cvg_sup. + by apply: fmap_filter; apply:nbhs_filter. +case=> K cptK /=. +move=> T /= [C1 [[C2 oR <- /= Rxcf RT]]]. +move: oR; rewrite openE => /(_ _ Rxcf); case => C3 [E entE] EE' EKR. +rewrite nbhs_simpl /=. +move: entE => [O [/=]]. +move=> D dcpt <- IDE. +near=> z; apply/RT/EKR/EE'; case=> w Kiw; have Kw : K w by rewrite inE in Kiw. +apply: IDE; rewrite /= /set_val /= /eqincl /incl. +move: w Kw {Kiw C1 C2 Rxcf RT EKR C3 EE' O T}. near: z. +near_simpl; move/compact_near_coveringP/near_covering_withinP : (cptK). +move=> /(_ _ (nbhs f)); apply => /= u Ku. +apply: filter_bigI_within; case; case; case => /= J cptJ L /= /[dup] /asboolP entL ? _. +case: entL => C1 [R /= entR] RC1 C1L. +exists (setT, [set g | forall pq, (K `*` J) pq -> R (f pq, g pq)]). + split; last apply: fam_nbhs => //; last exact: compact_setM. + apply: filterT. +case=> a g /= [? pJR] Ka. +apply: C1L; apply: RC1; rewrite /map_pair; case=> v /= Jiv. +rewrite /= /set_val /= /eqincl /incl. +by apply: pJR; split => //; rewrite inE in Jiv. +Unshelve. all: by end_near. Qed. +End currying. +(* +Lemma uncurry_continuous (f : U ~> V ~> W) : + locally_compact [set: V] -> + continuous f -> + (forall u, continuous (f u)) -> + {for f, continuous ((uncurry : (U ~> V ~> W) -> (U * V ~> W)))}. +Proof. +*) From 56c35524051852a336f515991890fae34c79c7cf Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 24 Apr 2023 21:06:59 -0400 Subject: [PATCH 06/15] performance --- theories/topology.v | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 84e63a2dac..10a0f4aa1f 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -8329,14 +8329,12 @@ exact. Qed. Section currying. +Context {U V W : uniformType}. Local Notation "U '~>' V" := ({family compact, [topologicalType of U] -> [uniformType of V]}) (at level 99, right associativity). -Section currying_pt1. -Context {U V W : uniformType}. - Lemma continuous_snd (f : U ~> V ~> W) v : continuous f -> (forall u, continuous (f u)) -> @@ -8413,19 +8411,16 @@ Lemma curry_continuous (f : U * V ~> W) : Proof. move=> ctsf; apply/cvg_sup. by apply: fmap_filter; apply:nbhs_filter. -case=> K cptK /=. -move=> T /= [C1 [[C2 oR <- /= Rxcf RT]]]. +case=> K cptK T [C1 [[C2 oR <- Rxcf RT]]]. move: oR; rewrite openE => /(_ _ Rxcf); case => C3 [E entE] EE' EKR. -rewrite nbhs_simpl /=. -move: entE => [O [/=]]. -move=> D dcpt <- IDE. +move: entE => [O []] => D dcpt <- IDE; rewrite nbhs_simpl /=. near=> z; apply/RT/EKR/EE'; case=> w Kiw; have Kw : K w by rewrite inE in Kiw. apply: IDE; rewrite /= /set_val /= /eqincl /incl. -move: w Kw {Kiw C1 C2 Rxcf RT EKR C3 EE' O T}. near: z. +move: w Kw {Kiw C1 C2 Rxcf RT EKR C3 EE' O T}; near: z. near_simpl; move/compact_near_coveringP/near_covering_withinP : (cptK). -move=> /(_ _ (nbhs f)); apply => /= u Ku. -apply: filter_bigI_within; case; case; case => /= J cptJ L /= /[dup] /asboolP entL ? _. -case: entL => C1 [R /= entR] RC1 C1L. +move=> /(_ _ (nbhs f)); apply => u Ku. +apply: filter_bigI_within; (do 3 case) => J cptJ L /[dup] /asboolP entL ? _. +case: entL => C1 [R entR] RC1 C1L. exists (setT, [set g | forall pq, (K `*` J) pq -> R (f pq, g pq)]). split; last apply: fam_nbhs => //; last exact: compact_setM. apply: filterT. From 6e2f556ee9f1540c1936bf0f3619af5d78216dbf Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 24 Apr 2023 21:15:44 -0400 Subject: [PATCH 07/15] moving proofs around working through uncurry compact-open topology working working through uncurry --- theories/topology.v | 567 +++++++++++++++++++++++++++++++------------- 1 file changed, 405 insertions(+), 162 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 10a0f4aa1f..1b15ea9ff7 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -553,6 +553,10 @@ Reserved Notation "{ 'family' fam , U -> V }" (at level 0, U at level 69, format "{ 'family' fam , U -> V }"). Reserved Notation "{ 'family' fam , F --> f }" (at level 0, F at level 69, format "{ 'family' fam , F --> f }"). +Reserved Notation "{ 'compact-open' , U -> V }" + (at level 0, U at level 69, format "{ 'compact-open' , U -> V }"). +Reserved Notation "{ 'compact-open' , F --> f }" + (at level 0, F at level 69, format "{ 'compact-open' , F --> f }"). Set Implicit Arguments. Unset Strict Implicit. @@ -1621,6 +1625,12 @@ Qed. #[global] Typeclasses Opaque within. +Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) + (F : set (set T)) (P : set T) : + Filter F -> (forall i, i \in D -> F ([set j | P j -> f i j])) -> + F ([set j | P j -> (\bigcap_(i in [set i | i \in D]) f i) j]). +Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. + Canonical within_filter_on T D (F : filter_on T) := FilterType (within D F) (within_filter _ _). @@ -1628,6 +1638,12 @@ Definition subset_filter {T} (F : set (set T)) (D : set T) := [set P : set {x | D x} | F [set x | forall Dx : D x, P (exist _ x Dx)]]. Arguments subset_filter {T} F D _. +Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) + (F : set (set T)) (P : set T) : + Filter F -> (forall i, i \in D -> F ([set j | P j -> f i j])) -> + F ([set j | P j -> (\bigcap_(i in [set i | i \in D]) f i) j]). +Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. + Global Instance subset_filter_filter T F (D : set T) : Filter F -> Filter (subset_filter F D). Proof. @@ -1709,6 +1725,41 @@ Qed. End NearSet. +Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set (set T)) + (P : (set U) -> Prop) : + ProperFilter F -> + (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> + (\forall y \near powerset_filter_from F, P (f @` y)). +Proof. +move=> FF [] G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from F). + by apply: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. +near=> M; apply: GP; apply: (Gs D) => //. + apply: filterS; first exact: preimage_image. + by apply: (near (near_small_set _) M). +have : M `<=` f @^-1` D by apply: (near (small_set_sub FfD) M). +by move/image_subset/subset_trans; apply; apply: image_preimage_subset. +Unshelve. all: by end_near. Qed. + +Lemma near_map_powerset {T U : Type} (f : T -> U) (F : set (set T)) + (P : (set U) -> Prop) : + (forall X Y, X `<=` Y -> P Y -> P X) -> + ProperFilter F -> + (\forall y \near powerset_filter_from F, P (f @` y)) -> + (\forall y \near powerset_filter_from (f x @[x --> F]), P y). +Proof. +move=> Psub FF [] G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). + by apply: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. +have ffiD : fmap f F (f@` D). + by rewrite /fmap /=; apply: filterS; first exact: preimage_image. +near=> M; have FfM : (fmap f F M) by apply (near (near_small_set _) M). +apply: (@Psub _ (f@`D)); first exact: (near (small_set_sub ffiD) M). +exact: GP. +Unshelve. all: by end_near. Qed. + Section PrincipalFilters. Definition principal_filter {X : Type} (x : X) : set (set X) := @@ -2492,6 +2543,24 @@ End Prod_Topology. (** Topology on matrices *) +Lemma fst_open {U V : topologicalType} (A : set (U * V)) : + open A -> open (fst @` A). +Proof. +rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [Pa ?] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => //. +move=> p Pp; exists (p, b) => //; apply: pqA; split => //. +exact: nbhs_singleton. +Qed. + +Lemma snd_open {U V : topologicalType} (A : set (U * V)) : + open A -> open (snd @` A). +Proof. +rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [? Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => //. +move=> q Qq; exists (a, q) => //; apply: pqA; split => //. +exact: nbhs_singleton. +Qed. + Section matrix_Topology. Variables (m n : nat) (T : topologicalType). @@ -2998,6 +3067,7 @@ by apply: filter_ex; [exact: PF| exact: filterI]. Qed. End Compact. + Arguments hausdorff_space : clear implicits. Section ClopenSets. @@ -3080,8 +3150,47 @@ Proof. by split; [exact: compact_near_covering| exact: near_covering_compact]. Qed. +Definition near_covering_within (K : set X) := + forall (I : Type) (F : set (set I)) (P : I -> X -> Prop), + Filter F -> + (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> + \near F, K `<=` P F. + +Lemma near_covering_withinP (K : set X): + near_covering_within K <-> near_covering K. +Proof. +split. + move=> cvrW I F P FF cvr. + near=> i; suff : K `<=` (fun q : X => K q -> P i q). + by move=> KKP k Kk; apply: KKP. + near: i; apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app. + by near=> j => /=. +move=> cvrW I F P FF cvr. +near=> i; suff : K `<=` (fun q : X => K q -> P i q). + by move=> KKP k Kk; apply: KKP. +near: i. +have := (cvrW I F (fun i q => K q -> P i q) FF). +apply => x Kx; have := cvr x Kx; apply: filter_app. +by near=> j => + ?; apply. +Unshelve. all: by end_near. Qed. + End near_covering. +Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) : + compact P -> compact Q -> compact (P `*` Q). +Proof. +rewrite ?compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. +have := cptP I F (fun i u => forall q, Q q -> Pr i (u,q)) Ff. +set R := (R in (R -> _) -> _); suff R' : R. + by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. +rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)). +move=> v Qv. +case: (cvfPQ (x,v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. +exists (N2,(N1`*`G)); first by split => //; exists (N1, G) => //. +case=> a [b i] /= [? [?]] ?. +by apply: (ngPr (b,a, i)); split => //; apply: N1N2N. +Unshelve. all: by end_near. Qed. + Section Tychonoff. Class UltraFilter T (F : set (set T)) := { @@ -6579,6 +6688,173 @@ move=> entE famA; have /fam_cvgP /(_ A) : (nbhs f --> f) by []; apply => //. by apply uniform_nbhs; exists E; split. Qed. +Lemma fam_compact_nbhs {U : topologicalType} {V : uniformType} + (A : set U) (O : set V) (f : {family compact, U -> V}) : + open O -> (f @` A `<=` O) -> compact A -> continuous f -> + nbhs (f : {family compact, U -> V}) [set g | forall y, A y -> O (g y)]. +Proof. +move=> oO fAO /[dup] ? /compact_near_coveringP/near_covering_withinP cfA ctsf. +near=> z => /=; (suff : A `<=` [set y | O (z y)] by exact); near: z. +apply: cfA => x Ax; have : O (f x) by apply: fAO. +move: (oO); rewrite openE /= => /[apply] /[dup] /ctsf Ofx /=. +rewrite /interior -nbhs_entourageE; case => E entE EfO. +exists (f @^-1` (to_set (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) => //=; last exact: AEg. +Unshelve. all: by end_near. Qed. + +(* It turns out {family compact, U -> V} can be generalized to only assume *) +(* `topologicalType` on V. This topology is called the compact-open topology. *) +(* This topology is special becaise its the _only_ topology that will allow *) +(* curry/uncurry to be continuous. *) + +Section compact_open. + +Context {T U : topologicalType}. + +Definition compact_open := (T->U)^o. + +Section compact_open_setwise. +Context {K : set T}. + +Definition compact_openK := let _ := K in compact_open. + +Definition compact_openK_nbhs (f : compact_openK) := + filter_from + [set O | f @` K `<=` O /\ open O] + (fun O => [set g | g @` K `<=` O]). + +Global Instance compact_openK_nbhs_filter (f : compact_openK) : + ProperFilter (compact_openK_nbhs f). +Proof. +split; first by case=> g [gKO oO] /(_ f); apply. +apply: filter_from_filter; first by exists setT; split => //; exact: openT. +move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split. +- by move=> ? [z Kz M-]; split; [apply: fKP | apply: fKQ]; exists z. +- exact: openI. +by move=> g /= gPQ; split; apply: (subset_trans gPQ) => ? []. +Qed. + +Program Definition compact_openK_topological_mixin : + Topological.mixin_of compact_openK_nbhs := + @Topological.Mixin compact_openK compact_openK_nbhs + (@open_of_nbhs _ compact_openK_nbhs) _ _ _. +Next Obligation. +move=> f; rewrite eqEsubset; split => A /=. + case=> B /= [fKB oB gKBA]; exists [set g | g @` K `<=` B]; split => //. + by move=> h /= hKB; exists B. +by case=> B [oB Bf /filterS]; apply; apply: oB. +Qed. +Next Obligation. done. Qed. + +Canonical compact_openK_filter := FilteredType + compact_openK compact_openK compact_openK_nbhs. +Canonical compact_openK_topological := TopologicalType + compact_openK compact_openK_topological_mixin. +End compact_open_setwise. + +Canonical compact_open_pointedType : pointedType := + PointedType compact_open point. + +Definition compact_open_topologicalType : topologicalType := + @sup_topologicalType _ (sigT (@compact T)) + (fun K => Topological.class (@compact_openK_topological (projT1 K))). + +Canonical compact_open_filtered := + [filteredType compact_open of compact_open for compact_open_topologicalType]. + +Canonical compact_open_topological := + [topologicalType of compact_open for compact_open_topologicalType]. + +Lemma compact_open_cvgP (F : set (set (compact_open_topological))) + (f : compact_open_topological) : + Filter F -> + (F --> f) <-> (forall K O, @compact T K -> @open U O -> f @` K `<=` O -> + F [set g | g @` K `<=` O] ). +Proof. +move=> FF; split. + by move/cvg_sup => + K O cptK ? ? => /(_ (existT _ _ cptK)); apply; exists O. +move=> fko; apply/cvg_sup; case=> A cptK O /= [C /= [fAC oC]]. +by move/filterS; apply; apply: fko. +Qed. + +Lemma compact_open_open (K : set T) (O : set U) : + compact K -> open O -> open ([set g | g @` K `<=` O] : set compact_open). +Proof. +pose C := [set g | g @` K `<=` O]; move=> cptK oO. +exists [set C]; last by rewrite bigcup_set1. +move=> ? ->; exists (fset1 C) => //; last by rewrite set_fset1 bigcap_set1. +by move=> ?; rewrite ?inE => ->; exists (existT _ _ cptK) => // z Cz; exists O. +Qed. + +End compact_open. + +Lemma compact_closedI {T : topologicalType} (A B : set T) : + compact A -> closed B -> compact (A `&` B). +Proof. +move=> cptA clB F PF FAB; have FA : F A by move: FAB; apply: filterS. +(have FB : F B by move: FAB; apply: filterS); have [x [Ax]] := cptA F PF FA. +move=> /[dup] clx; rewrite {1}clusterE => /(_ (closure B)); move: clB. +by rewrite closure_id => /[dup] + <- => <- /(_ FB) Bx; exists x; split. +Qed. + +Notation "{ 'compact-open' , U -> V }" := (@compact_open U V). +Notation "{ 'compact-open' , F --> f }" := + (F --> (f : @compact_open_topological _ _)). + +Section compact_open_uniform. +Context {U : topologicalType} {V : uniformType}. + +Let small_ent_sub := @small_set_sub _ (@entourage V). + +Lemma compact_open_fam_compactP (f : U -> V) (F : set (set (U -> V))) : + continuous f -> (Filter F) -> + {compact-open, F --> f} <-> {family compact, F --> f}. +Proof. +move=> ctsf FF; split. + move/compact_open_cvgP=> cptOF; apply/cvg_sup; case=> K cptK R. + case=> D /= [[E oE <- /=] Ekf] /filterS; apply. + move: oE; rewrite openE => /(_ _ Ekf); case => ? [J entJ /=] EKR KfE. + near=> z; apply/KfE/EKR; case => u /= Kp. + rewrite /= /set_val /= /eqincl /incl/set_val /= /comp. + (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))%classic. + pose B := \bigcup_(z in K `&` closure C) interior (to_set E' (f z)). + have oB : open B by apply: bigcup_open => ? ?; exact: open_interior. + have fKB : f @` (K `&` closure C) `<=` B. + move=> ? [z ? <-]; exists z => //; rewrite /interior. + by rewrite -nbhs_entourageE; exists E'. + have cptKC : compact (K `&` closure C). + apply: compact_closedI => //; exact: closed_closure. + have := cptOF (K `&` closure C) B cptKC oB fKB. + exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). + split. + - by apply: (ctsf) => //; rewrite /filter_of -nbhs_entourageE; exists E'. + - exact: cptOF. + - case=> z h /= [Cz KB Kz]. + case: (KB (h z)); first by (exists z; split => //; apply: subset_closure). + move=> w [Kw Cw /interior_subset Jfwhz]; apply:subset_split_ent => //. + exists (f w); last apply:(near (small_ent_sub _) E') => //. + apply: subset_split_ent => //; exists (f u). + apply entourage_sym; apply:(near (small_ent_sub _) E') => //. + have [] := Cw (f@^-1` (to_set E' (f w))). + by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. + move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r). + by apply:(near (small_ent_sub _) E') => //. + by apply entourage_sym; apply:(near (small_ent_sub _) E') => //. +move=> cptF; apply/compact_open_cvgP => K O cptK oO fKO. +apply: cptF; have := fam_compact_nbhs oO fKO cptK ctsf; apply: filter_app. +by near=> g => /= gKO ? [z Kx <-]; apply: gKO. +Unshelve. all: by end_near. Qed. + +End compact_open_uniform. + Definition compactly_in {U : topologicalType} (A : set U) := [set B | B `<=` A /\ compact B]. @@ -7632,7 +7908,7 @@ move/filterS; apply; have [//|i nclfix] := @sepf _ x (open_closedC oB). apply: (wiFx i); have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); [split=>//|]. apply: open_comp; last by rewrite ?openC; last apply: closed_closure. - by move=> + _; exact: weak_continuous. + by move=> + _; exact: (@weak_continuous _ _ (f_ i)). rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. by move/forall2NP => /(_ z) [] // /contrapT. Qed. @@ -8210,141 +8486,21 @@ Qed. End ArzelaAscoli. -Lemma fst_open {U V : topologicalType} (A : set (U * V)) : - open A -> open (fst @` A). -Proof. -rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. -have [[P Q] [Pa ?] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => //. -move=> p Pp; exists (p, b) => //; apply: pqA; split => //. -exact: nbhs_singleton. -Qed. - -Lemma snd_open {U V : topologicalType} (A : set (U * V)) : - open A -> open (snd @` A). -Proof. -rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. -have [[P Q] [? Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => //. -move=> q Qq; exists (a, q) => //; apply: pqA; split => //. -exact: nbhs_singleton. -Qed. - -Lemma near_powerset_map {T U : topologicalType} (f : T -> U) (F : set (set T)) - (P : (set U) -> Prop) : - ProperFilter F -> - (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> - (\forall y \near powerset_filter_from F, P (f @` y)). -Proof. -move=> FF [] G /= [Gf Gs [D GD GP]]. -have PpF : ProperFilter (powerset_filter_from F). - by apply: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. -near=> M; apply: GP; apply: (Gs D) => //. - apply: filterS; first exact: preimage_image. - by apply: (near (near_small_set _) M). -have : M `<=` f @^-1` D by apply: (near (small_set_sub FfD) M). -by move/image_subset/subset_trans; apply; apply: image_preimage_subset. -Unshelve. all: by end_near. Qed. - -Lemma near_map_powerset {T U : topologicalType} (f : T -> U) (F : set (set T)) - (P : (set U) -> Prop) : - (forall X Y, X `<=` Y -> P Y -> P X) -> - ProperFilter F -> - (\forall y \near powerset_filter_from F, P (f @` y)) -> - (\forall y \near powerset_filter_from (f x @[x --> F]), P y). -Proof. -move=> Psub FF [] G /= [Gf Gs [D GD GP]]. -have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). - by apply: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. -have ffiD : fmap f F (f@` D). - by rewrite /fmap /=; apply: filterS; first exact: preimage_image. -near=> M; have FfM : (fmap f F M) by apply (near (near_small_set _) M). -apply: (@Psub _ (f@`D)); first exact: (near (small_set_sub ffiD) M). -exact: GP. -Unshelve. all: by end_near. Qed. - -Lemma continuous_fst_arg {U V W : topologicalType} (f : U * V -> W) (u : U) : - continuous f -> continuous (curry f u). -Proof. -move=> ctsf; rewrite (_ : curry f u = f \o (pair u)); last exact:funext. -move=> y; apply: continuous_comp; last exact: ctsf. -by apply: cvg_pair; [exact: cvg_cst | exact: cvg_id]. -Qed. - -Lemma continuous_snd_arg {U V W : topologicalType} (f : U * V -> W) (v : V) : - continuous f -> continuous (fun q => curry f q v). -Proof. -move=> ctsf; suff : continuous (f \o (fun q => pair q v)) by exact. -move=> y; apply: continuous_comp; last exact: ctsf. -by apply: cvg_pair; [exact: cvg_id | exact: cvg_cst]. -Qed. - -Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) : - compact P -> compact Q -> compact (P `*` Q). -Proof. -rewrite ?compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. -have := cptP I F (fun i u => forall q, Q q -> Pr i (u,q)) Ff. -set R := (R in (R -> _) -> _); suff R' : R. - by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. -rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)). -move=> v Qv. -case: (cvfPQ (x,v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. -exists (N2,(N1`*`G)); first by split => //; exists (N1, G) => //. -case=> a [b i] /= [? [?]] ?. -by apply: (ngPr (b,a, i)); split => //; apply: N1N2N. -Unshelve. all: by end_near. Qed. - -Definition near_covering_within {X : topologicalType} (K : set X) := - forall (I : Type) (F : set (set I)) (P : I -> X -> Prop), - Filter F -> - (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> - \near F, K `<=` P F. - -Lemma near_covering_withinP {X : topologicalType} (K : set X): - near_covering_within K <-> near_covering K. -Proof. -split. - move=> cvrW I F P FF cvr. - near=> i; suff : K `<=` (fun q : X => K q -> P i q). - by move=> KKP k Kk; apply: KKP. - near: i; apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app. - by near=> j => /=. -move=> cvrW I F P FF cvr. -near=> i; suff : K `<=` (fun q : X => K q -> P i q). - by move=> KKP k Kk; apply: KKP. -near: i. -have := (cvrW I F (fun i q => K q -> P i q) FF). -apply => x Kx; have := cvr x Kx; apply: filter_app. -by near=> j => + ?; apply. -Unshelve. all: by end_near. Qed. - -Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set (set T)) (P : set T) : - Filter F -> (forall i, i \in D -> F ([set j | P j -> f i j])) -> - F ([set j | P j -> (\bigcap_(i in [set i | i \in D]) f i) j]). -Proof. -move=> FF FfD. -have := @filter_bigI T I D f (within P F) (within_filter P FF). -exact. -Qed. - Section currying. -Context {U V W : uniformType}. - Local Notation "U '~>' V" := - ({family compact, [topologicalType of U] -> [uniformType of V]}) - (at level 99, right associativity). + ({compact-open, [topologicalType of U] -> [topologicalType of V]}) + (at level 99, right associativity). -Lemma continuous_snd (f : U ~> V ~> W) v : - continuous f -> +Context {U V W : topologicalType}. + +(* +Lemma continuous_snd (f : U ~> V ~> W) (v : V) : + continuous f -> (forall u, continuous (f u)) -> - continuous (fun q => f q v). + continuous (fun (q : U) => f q v). Proof. -move=> ctsf ctsfp x ?. -rewrite /= -nbhs_entourageE; case=> E entE /filterS; apply. -rewrite ?nbhs_simpl /=; near=> z => /=; near: z. -near (powerset_filter_from (@entourage W)) => E'. -have entE' : entourage E' by exact: (near (near_small_set _)). +move=> ctsf ctsfp x R /= fxvR; rewrite nbhs_simpl /=. +near=> z => /=; near: z. have nvE' : nbhs v (f x @^-1` (to_set E' (f x v))). by apply: ctsfp; rewrite /= -nbhs_entourageE; exists E'. suff [O Ofx OE] : exists2 O, nbhs (f x) O & (forall g, O g -> E (f x v, g v)). @@ -8354,43 +8510,55 @@ exists [set g | forall z, [set v] z -> E (f x z, g z)]. by apply: fam_nbhs => //; exact: compact_set1. by move=> g; apply. Unshelve. all: by end_near. Qed. +*) Lemma continuous_curry (f : U * V ~> W) : - continuous f -> continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)) f). -Proof. -move=> ctsf x; apply/cvg_sup; case => K cptK /=. -have Pfx : ProperFilter (powerset_filter_from (curry f x @[x --> x])). - apply: powerset_filter_from_filter. -have Pfx2 : ProperFilter (powerset_filter_from (nbhs (curry f x))). - apply: powerset_filter_from_filter. -move=> T /= [? [[? oR <- /= Rxcf RT]]]. -move: oR; rewrite openE => /(_ _ Rxcf); case => ? [E entE] EE' EKR. -near=> z; apply/RT/EKR/EE'; case=> w Kiw; have Kw : K w by rewrite inE in Kiw. -rewrite /= /set_val /= /eqincl /incl; move: w Kw {Kiw}; near: z. -rewrite nbhs_simpl; near_simpl; move/compact_near_coveringP : cptK; apply. -move=> v Kv /=. -near (powerset_filter_from (@entourage W)) => E'. -have entE' : entourage E' by exact: (near (near_small_set _)). -have : nbhs (x,v) (f @^-1` to_set E' (f (x,v))). - by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. -case; case=> /= P Q [Px Qy] PQfE. -exists (Q,P); first by split => //. -case=> b a [/=] Qb Pa; rewrite /curry; apply: subset_split_ent => //. -exists (f (x,v)); last by apply: (near (small_ent_sub _) E') => //; apply: PQfE. -rewrite /fst. -apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. -apply: PQfE; split => //; exact: nbhs_singleton. + continuous f -> continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)) f). +Proof. +move=> ctsf x; apply/compact_open_cvgP => K O /= cptK oO fKO. +near=> z => /= w /= [+ + <-]; near: z. +move/compact_near_coveringP/near_covering_withinP: cptK; apply. +move=> v Kv; have [[P Q] [Px Qv] PQfO]: nbhs (x,v) (f@^-1` O). + by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. +by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; apply: PQfO. Unshelve. all: by end_near. Qed. Lemma continuous_uncurry (f : U ~> V ~> W): locally_compact [set: V] -> + hausdorff_space V -> continuous f -> (forall u, continuous (f u)) -> continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). Proof. -move=> lcV ctsf ctsfp /= [u v] D /=; rewrite -nbhs_entourageE. -case => E entE /filterS; apply. +move=> lcV ctsf ctsfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv]. +move/filterS; apply. have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. +have [G [gv EG2 [M GM GO]]] : \forall C \near powerset_filter_from (nbhs v), + forall z, closure C z -> O (f u z). + move/compact_near_coveringP/near_covering_withinP: cptB; apply=> z Bz. + have [K] := @lcV z I; rewrite withinET; move=> Kz [cptK clK]. + + +exists (f @^-1` ([set g | g @` (B `&` closure M) `<=` O]), (B `&` closure M)). + split; [apply/ctsf/open_nbhs_nbhs; split | apply: filterI]. + - apply: compact_open_open => //; apply: compact_closedI => //. + exact: closed_closure. + - by move=> ? [x [? + <-]]; apply: GO. + - done. + - by apply: filterS; [exact: subset_closure|]; exact: gv. +by case=> a r /= [fBMO [Br] cmR]; apply: fBMO; exists r. +simpl. + +pose B' := B `&` closure . +rewrite /nbhs /=; near=> z => /=; near: z. +have : nbhs u (f @^-1` [set g | g @` B' `<=` O]). + exact: closed_closure. + move=> z [? [? clfO] <-]. + + + +have : nbhs (curry f u) ([set g | g @` B `<=` O]). + apply: ctsf; apply: compact_open_nbhs => //. near (powerset_filter_from (@entourage W)) => E'. have entE' : entourage E' by exact: (near (near_small_set _)). have /ctsf /= cfN := @fam_nbhs _ _ _ B _ (f u : V ~> W) entE' cptB. @@ -8405,7 +8573,7 @@ apply: subset_split_ent => //; exists (f u b) => /=. by apply: (near (small_ent_sub _) E') => //; apply: Eua. Unshelve. all: by end_near. Qed. -Lemma curry_continuous (f : U * V ~> W) : +Lemma curry_continuous (f : U * V ~> W) : continuous f -> {for f, continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)))}. Proof. @@ -8430,13 +8598,88 @@ rewrite /= /set_val /= /eqincl /incl. by apply: pJR; split => //; rewrite inE in Jiv. Unshelve. all: by end_near. Qed. -End currying. -(* Lemma uncurry_continuous (f : U ~> V ~> W) : locally_compact [set: V] -> continuous f -> (forall u, continuous (f u)) -> {for f, continuous ((uncurry : (U ~> V ~> W) -> (U * V ~> W)))}. Proof. -*) - +move=> lcV ctsf ctsfp; apply/cvg_sup. + by apply: fmap_filter; apply:nbhs_filter. +case=> K cptK T [C1 [[C2 oR <- Rxcf RT]]]. +move: oR; rewrite openE => /(_ _ Rxcf); case => C3 [E entE] EE' EKR. +rewrite nbhs_simpl /=. +near=> z; apply/RT/EKR/EE'; case=> w Kiw; have Kw : K w by rewrite inE in Kiw. +rewrite /= /set_val /= /eqincl /incl. +move: w Kw {Kiw C1 C2 Rxcf RT EKR C3 EE' T}; near: z. +near_simpl; move/compact_near_coveringP/near_covering_withinP : (cptK). +near (powerset_filter_from (@entourage W)) => E'. +have entE' : entourage E' by exact: (near (near_small_set _)). +move=> /(_ _ (nbhs f)); apply; case => u v Kxy. +have ectsf : equicontinuous (f @` (fst @` K)) id. + apply: compact_equicontinuous => //. + by move=> ? [? [? ? <- <-]]; apply: ctsfp. + apply: continuous_compact; first exact: continuous_subspaceT. + apply: continuous_compact => //; apply: continuous_subspaceT => ?; exact: cvg_fst. +have Efv : forall b, \forall y \near b, forall a, (fst @` K) a -> E' (f a b, f a y). + move=> b; move: (ectsf b E' entE'). + apply: filter_app; near=> z => + a [[? r /[swap] /= ->] Kab]. + by apply; exists a => //; exists (a,r). +have cptK2 : compact (snd @` K). + apply: continuous_compact => //; apply: continuous_subspaceT => ?; exact: cvg_snd. +have : \forall y \near v, forall b, (snd @` K) b -> (forall a, (fst @` K) a -> E' (f a b, f a y)). + move/compact_near_coveringP/near_covering_withinP: cptK2. + apply=> // z K2z; have := Efv z E' entE'. + +exists ( + (((f^~ v) @^-1` to_set E' (f u v)) `*` + [set y | forall b, (fst @` K) b -> E' (f b v, f b y)]), + [set g | forall ab, K ab -> E' (f u v, g ab.1 ab.2)]); first last. + case; case => /= a b g [[fvE' P1b] fgE'] Kab. + apply: subset_split_ent => //; exists (f a v) => /=. + apply/entourage_sym; apply: (near (small_ent_sub _) E') => //; apply: P1b. + by exists (a,b). + apply: subset_split_ent => //; exists (f u v) => /=. + apply/entourage_sym; apply: (near (small_ent_sub _) E') => //; apply: fvE'. + by apply: (near (small_ent_sub _) E') => //; apply: (fgE' (a,b)). +split; first exists + (((f^~ v) @^-1` to_set E' (f u v)), + [set y | forall b, (fst @` K) b -> E' (f b v, f b y)]) => //=. + split => //; apply: continuous_snd => //; rewrite /= -nbhs_entourageE. + by exists E'. +rewrite nbhs_simpl /=. + + exists (((f^~ v) @^-1` to_set E' (f u v)), P1) => //; split => //. + by apply: continuous_snd => //=. +rewrite nbhs_simpl /=. +suff : [set g | forall a, (fst @` K) a -> N (f a, g a) ]`<=` + [set g | forall a b, K (a , b) -> E'(f u v, g a b) ]. + move/filterS; apply; apply: fam_nbhs => //; apply: continuous_compact => //. + by apply: continuous_subspaceT => ?; exact: cvg_fst. +move=> g /= fa a b Kab. +apply: fa. +have : nbhs f [set g | forall a b, (fst @` K) -> ] + + + + +have := P1b (g a). +case. +move: P1b; rewrite /P1 (g a). +have := Evcts. + +have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. +have fzE : forall z, nbhs (f z) [set g | forall w, B w -> E (f z w, g w)]. + move=> z; apply: fam_nbhs => //. +move: (fzE u); rewrite -nbhs_entourageE; case=> R entR RBE. +have fE : nbhs f [set g | forall w, (fst @` K) w -> R (f w, g w)]. + apply: fam_nbhs=>//; + by apply: continuous_subspaceT => ?; apply: cvg_fst. +exists ((setT `*` B), [set g | forall w, (fst @` K) w -> R (f w, g w)]). + split => //; exists (setT, B) => //; split => //; exact: filterT. +case;case=> a b /= g [[_ Bb] wKR] KAB. +have /= := (RBE (f a)). +have : nbhs f [set g | forall z, fst @` K z -> ] + + +End currying. \ No newline at end of file From df5a1a3a8a347084608808ea17fe690bfd8014d3 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 1 May 2023 10:38:54 -0400 Subject: [PATCH 08/15] uncurry continuous part 1 --- theories/topology.v | 82 +++++++++++++++++++++++++-------------------- 1 file changed, 45 insertions(+), 37 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 1b15ea9ff7..0c7e283396 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3380,7 +3380,6 @@ move=> M [MF ME2 [W] MW /(_ _ MW) VUW]. apply: (@filterS _ _ _ (V `&` W)); last by apply: filterI => //; exact: MF. by move=> t [Vt Wt]; apply: contrapT => Ut; exact: (VUW t). Qed. - Section Precompact. Context {X : topologicalType}. @@ -3664,6 +3663,9 @@ move=> /DsubC /= [y /= yfs hyz]; exists (h' y) => //. by rewrite set_imfset /=; exists y. Qed. +Definition regular {T : topologicalType} := forall (x:T), + (filter_from (nbhs x) closure) --> x. + Section separated_topologicalType. Variable (T : topologicalType). Implicit Types x y : T. @@ -3823,6 +3825,27 @@ Proof. move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl. Qed. +Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular}. +Proof. +move=> cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //. +- apply: filter_from_proper => //; first last. + by move=> ? /nbhs_singleton/subset_closure ?; exists x. + apply: filter_from_filter; first by exists setT; exact: filterT. + move=> P Q Px Qx; exists (P `&` Q); [exact: filterI | exact: closureI]. +- by exists V => //; have /closure_id <- : closed V by exact: compact_closed. +rewrite eqEsubset; split; first last. + move=> ? -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //. + by apply/CA/subset_closure; exact: nbhs_singleton. +move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply]. +case; case=> B A /=; rewrite ?inE; case=> By Ax [oB oA BA0]. +apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP. +split; first by exists A => //; apply: open_nbhs_nbhs. +apply/not_implyP; split; first by exact: open_nbhs_nbhs. +apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset. +have /closure_id -> : closed (~` B); first by exact: open_closedC. +by apply/closure_subset/disjoints_subset; rewrite setIC. +Qed. + End separated_topologicalType. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")] @@ -8523,55 +8546,40 @@ move=> v Kv; have [[P Q] [Px Qv] PQfO]: nbhs (x,v) (f@^-1` O). by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; apply: PQfO. Unshelve. all: by end_near. Qed. -Lemma continuous_uncurry (f : U ~> V ~> W): +Lemma continuous_uncurry_regular (f : U ~> V ~> W): locally_compact [set: V] -> - hausdorff_space V -> + @regular V -> continuous f -> (forall u, continuous (f u)) -> continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). Proof. -move=> lcV ctsf ctsfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv]. +move=> lcV reg ctsf ctsfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv]. move/filterS; apply. have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. -have [G [gv EG2 [M GM GO]]] : \forall C \near powerset_filter_from (nbhs v), - forall z, closure C z -> O (f u z). - move/compact_near_coveringP/near_covering_withinP: cptB; apply=> z Bz. - have [K] := @lcV z I; rewrite withinET; move=> Kz [cptK clK]. - - -exists (f @^-1` ([set g | g @` (B `&` closure M) `<=` O]), (B `&` closure M)). +have [R Rv RO] : exists2 R, nbhs v R & (forall z, closure R z -> O (f u z)). + have [] := reg v ((f u)@^-1` O); first by apply: ctsfp; exact: open_nbhs_nbhs. + by move=> R nR cRO; exists R. +exists (f @^-1` ([set g | g @` (B `&` closure R) `<=` O]), (B `&` closure R)). split; [apply/ctsf/open_nbhs_nbhs; split | apply: filterI]. - apply: compact_open_open => //; apply: compact_closedI => //. exact: closed_closure. - - by move=> ? [x [? + <-]]; apply: GO. + - by move=> ? [x [? + <-]]; apply: RO. - done. - - by apply: filterS; [exact: subset_closure|]; exact: gv. + - by apply: filterS; [exact: subset_closure|]. by case=> a r /= [fBMO [Br] cmR]; apply: fBMO; exists r. -simpl. - -pose B' := B `&` closure . -rewrite /nbhs /=; near=> z => /=; near: z. -have : nbhs u (f @^-1` [set g | g @` B' `<=` O]). - exact: closed_closure. - move=> z [? [? clfO] <-]. - - +Qed. -have : nbhs (curry f u) ([set g | g @` B `<=` O]). - apply: ctsf; apply: compact_open_nbhs => //. -near (powerset_filter_from (@entourage W)) => E'. -have entE' : entourage E' by exact: (near (near_small_set _)). -have /ctsf /= cfN := @fam_nbhs _ _ _ B _ (f u : V ~> W) entE' cptB. -exists ( - f@^-1`[set g | forall y, B y -> E' (f u y, g y)], - f u @^-1` (to_set E' (f u v)) `&` B). - split => //; apply: filterI => //; apply: ctsfp. - by rewrite /= -nbhs_entourageE /=; exists E'. -case=> a b /= [Eua [Evb Bb]]. -apply: subset_split_ent => //; exists (f u b) => /=. - apply: (near (small_ent_sub _) E') => //; apply: Mb; exists a => //. -by apply: (near (small_ent_sub _) E') => //; apply: Eua. -Unshelve. all: by end_near. Qed. +Lemma continuous_uncurry (f : U ~> V ~> W): + locally_compact [set: V] -> + hausdorff_space V -> + continuous f -> + (forall u, continuous (f u)) -> + continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). +Proof. +move=> lcV hsdf ? ?; apply: continuous_uncurry_regular => //. +move=> v; have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. +by move=> z; apply: (@compact_regular V hsdf v B). +Qed. Lemma curry_continuous (f : U * V ~> W) : continuous f -> From b7ac86bc8ec5b35d0b23e85915c8d65f375b48c3 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 1 May 2023 17:40:45 -0400 Subject: [PATCH 09/15] curry continuous with extra assumptions better conditions working through uncurry all the currying lemmas --- theories/topology.v | 322 ++++++++++++++++++++------------------------ 1 file changed, 146 insertions(+), 176 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 0c7e283396..9aa18fd2f0 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1625,25 +1625,19 @@ Qed. #[global] Typeclasses Opaque within. +Canonical within_filter_on T D (F : filter_on T) := + FilterType (within D F) (within_filter _ _). + Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) (F : set (set T)) (P : set T) : Filter F -> (forall i, i \in D -> F ([set j | P j -> f i j])) -> F ([set j | P j -> (\bigcap_(i in [set i | i \in D]) f i) j]). Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. -Canonical within_filter_on T D (F : filter_on T) := - FilterType (within D F) (within_filter _ _). - Definition subset_filter {T} (F : set (set T)) (D : set T) := [set P : set {x | D x} | F [set x | forall Dx : D x, P (exist _ x Dx)]]. Arguments subset_filter {T} F D _. -Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set (set T)) (P : set T) : - Filter F -> (forall i, i \in D -> F ([set j | P j -> f i j])) -> - F ([set j | P j -> (\bigcap_(i in [set i | i \in D]) f i) j]). -Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. - Global Instance subset_filter_filter T F (D : set T) : Filter F -> Filter (subset_filter F D). Proof. @@ -1726,12 +1720,12 @@ Qed. End NearSet. Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set (set T)) - (P : (set U) -> Prop) : + (P : (set U) -> Prop) : ProperFilter F -> - (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> + (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> (\forall y \near powerset_filter_from F, P (f @` y)). Proof. -move=> FF [] G /= [Gf Gs [D GD GP]]. +move=> FF [] G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from F). by apply: powerset_filter_from_filter. have /= := Gf _ GD; rewrite nbhs_simpl => FfD. @@ -1743,13 +1737,13 @@ by move/image_subset/subset_trans; apply; apply: image_preimage_subset. Unshelve. all: by end_near. Qed. Lemma near_map_powerset {T U : Type} (f : T -> U) (F : set (set T)) - (P : (set U) -> Prop) : + (P : (set U) -> Prop) : (forall X Y, X `<=` Y -> P Y -> P X) -> ProperFilter F -> (\forall y \near powerset_filter_from F, P (f @` y)) -> (\forall y \near powerset_filter_from (f x @[x --> F]), P y). Proof. -move=> Psub FF [] G /= [Gf Gs [D GD GP]]. +move=> Psub FF [] G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). by apply: powerset_filter_from_filter. have /= := Gf _ GD; rewrite nbhs_simpl => FfD. @@ -3156,10 +3150,10 @@ Definition near_covering_within (K : set X) := (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> \near F, K `<=` P F. -Lemma near_covering_withinP (K : set X): +Lemma near_covering_withinP (K : set X): near_covering_within K <-> near_covering K. Proof. -split. +split. move=> cvrW I F P FF cvr. near=> i; suff : K `<=` (fun q : X => K q -> P i q). by move=> KKP k Kk; apply: KKP. @@ -3169,7 +3163,7 @@ move=> cvrW I F P FF cvr. near=> i; suff : K `<=` (fun q : X => K q -> P i q). by move=> KKP k Kk; apply: KKP. near: i. -have := (cvrW I F (fun i q => K q -> P i q) FF). +have := (cvrW I F (fun i q => K q -> P i q) FF). apply => x Kx; have := cvr x Kx; apply: filter_app. by near=> j => + ?; apply. Unshelve. all: by end_near. Qed. @@ -3836,9 +3830,9 @@ move=> cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //. rewrite eqEsubset; split; first last. move=> ? -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //. by apply/CA/subset_closure; exact: nbhs_singleton. -move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply]. +move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply]. case; case=> B A /=; rewrite ?inE; case=> By Ax [oB oA BA0]. -apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP. +apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP. split; first by exists A => //; apply: open_nbhs_nbhs. apply/not_implyP; split; first by exact: open_nbhs_nbhs. apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset. @@ -6716,12 +6710,12 @@ Lemma fam_compact_nbhs {U : topologicalType} {V : uniformType} open O -> (f @` A `<=` O) -> compact A -> continuous f -> nbhs (f : {family compact, U -> V}) [set g | forall y, A y -> O (g y)]. Proof. -move=> oO fAO /[dup] ? /compact_near_coveringP/near_covering_withinP cfA ctsf. +move=> oO fAO /[dup] ? /compact_near_coveringP/near_covering_withinP cfA ctsf. near=> z => /=; (suff : A `<=` [set y | O (z y)] by exact); near: z. -apply: cfA => x Ax; have : O (f x) by apply: fAO. -move: (oO); rewrite openE /= => /[apply] /[dup] /ctsf Ofx /=. +apply: cfA => x Ax; have : O (f x) by apply: fAO. +move: (oO); rewrite openE /= => /[apply] /[dup] /ctsf Ofx /=. rewrite /interior -nbhs_entourageE; case => E entE EfO. -exists (f @^-1` (to_set (split_ent E) (f x)), +exists (f @^-1` (to_set (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). @@ -6745,12 +6739,12 @@ Context {K : set T}. Definition compact_openK := let _ := K in compact_open. -Definition compact_openK_nbhs (f : compact_openK) := - filter_from - [set O | f @` K `<=` O /\ open O] +Definition compact_openK_nbhs (f : compact_openK) := + filter_from + [set O | f @` K `<=` O /\ open O] (fun O => [set g | g @` K `<=` O]). -Global Instance compact_openK_nbhs_filter (f : compact_openK) : +Global Instance compact_openK_nbhs_filter (f : compact_openK) : ProperFilter (compact_openK_nbhs f). Proof. split; first by case=> g [gKO oO] /(_ f); apply. @@ -6761,9 +6755,9 @@ move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split. by move=> g /= gPQ; split; apply: (subset_trans gPQ) => ? []. Qed. -Program Definition compact_openK_topological_mixin : +Program Definition compact_openK_topological_mixin : Topological.mixin_of compact_openK_nbhs := - @Topological.Mixin compact_openK compact_openK_nbhs + @Topological.Mixin compact_openK compact_openK_nbhs (@open_of_nbhs _ compact_openK_nbhs) _ _ _. Next Obligation. move=> f; rewrite eqEsubset; split => A /=. @@ -6773,26 +6767,26 @@ by case=> B [oB Bf /filterS]; apply; apply: oB. Qed. Next Obligation. done. Qed. -Canonical compact_openK_filter := FilteredType +Canonical compact_openK_filter := FilteredType compact_openK compact_openK compact_openK_nbhs. -Canonical compact_openK_topological := TopologicalType +Canonical compact_openK_topological := TopologicalType compact_openK compact_openK_topological_mixin. End compact_open_setwise. -Canonical compact_open_pointedType : pointedType := +Canonical compact_open_pointedType : pointedType := PointedType compact_open point. -Definition compact_open_topologicalType : topologicalType := +Definition compact_open_topologicalType : topologicalType := @sup_topologicalType _ (sigT (@compact T)) (fun K => Topological.class (@compact_openK_topological (projT1 K))). -Canonical compact_open_filtered := +Canonical compact_open_filtered := [filteredType compact_open of compact_open for compact_open_topologicalType]. -Canonical compact_open_topological := +Canonical compact_open_topological := [topologicalType of compact_open for compact_open_topologicalType]. -Lemma compact_open_cvgP (F : set (set (compact_open_topological))) +Lemma compact_open_cvgP (F : set (set (compact_open_topological))) (f : compact_open_topological) : Filter F -> (F --> f) <-> (forall K O, @compact T K -> @open U O -> f @` K `<=` O -> @@ -6800,14 +6794,14 @@ Lemma compact_open_cvgP (F : set (set (compact_open_topological))) Proof. move=> FF; split. by move/cvg_sup => + K O cptK ? ? => /(_ (existT _ _ cptK)); apply; exists O. -move=> fko; apply/cvg_sup; case=> A cptK O /= [C /= [fAC oC]]. +move=> fko; apply/cvg_sup; case=> A cptK O /= [C /= [fAC oC]]. by move/filterS; apply; apply: fko. Qed. Lemma compact_open_open (K : set T) (O : set U) : compact K -> open O -> open ([set g | g @` K `<=` O] : set compact_open). Proof. -pose C := [set g | g @` K `<=` O]; move=> cptK oO. +pose C := [set g | g @` K `<=` O]; move=> cptK oO. exists [set C]; last by rewrite bigcup_set1. move=> ? ->; exists (fset1 C) => //; last by rewrite set_fset1 bigcap_set1. by move=> ?; rewrite ?inE => ->; exists (existT _ _ cptK) => // z Cz; exists O. @@ -6815,17 +6809,17 @@ Qed. End compact_open. -Lemma compact_closedI {T : topologicalType} (A B : set T) : +Lemma compact_closedI {T : topologicalType} (A B : set T) : compact A -> closed B -> compact (A `&` B). Proof. move=> cptA clB F PF FAB; have FA : F A by move: FAB; apply: filterS. -(have FB : F B by move: FAB; apply: filterS); have [x [Ax]] := cptA F PF FA. -move=> /[dup] clx; rewrite {1}clusterE => /(_ (closure B)); move: clB. +(have FB : F B by move: FAB; apply: filterS); have [x [Ax]] := cptA F PF FA. +move=> /[dup] clx; rewrite {1}clusterE => /(_ (closure B)); move: clB. by rewrite closure_id => /[dup] + <- => <- /(_ FB) Bx; exists x; split. Qed. Notation "{ 'compact-open' , U -> V }" := (@compact_open U V). -Notation "{ 'compact-open' , F --> f }" := +Notation "{ 'compact-open' , F --> f }" := (F --> (f : @compact_open_topological _ _)). Section compact_open_uniform. @@ -6834,10 +6828,10 @@ Context {U : topologicalType} {V : uniformType}. Let small_ent_sub := @small_set_sub _ (@entourage V). Lemma compact_open_fam_compactP (f : U -> V) (F : set (set (U -> V))) : - continuous f -> (Filter F) -> + continuous f -> (Filter F) -> {compact-open, F --> f} <-> {family compact, F --> f}. Proof. -move=> ctsf FF; split. +move=> ctsf FF; split. move/compact_open_cvgP=> cptOF; apply/cvg_sup; case=> K cptK R. case=> D /= [[E oE <- /=] Ekf] /filterS; apply. move: oE; rewrite openE => /(_ _ Ekf); case => ? [J entJ /=] EKR KfE. @@ -6847,26 +6841,26 @@ move=> ctsf FF; split. 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))%classic. + pose C := f@^-1`(to_set E' (f u))%classic. pose B := \bigcup_(z in K `&` closure C) interior (to_set E' (f z)). have oB : open B by apply: bigcup_open => ? ?; exact: open_interior. have fKB : f @` (K `&` closure C) `<=` B. - move=> ? [z ? <-]; exists z => //; rewrite /interior. + move=> ? [z ? <-]; exists z => //; rewrite /interior. by rewrite -nbhs_entourageE; exists E'. have cptKC : compact (K `&` closure C). apply: compact_closedI => //; exact: closed_closure. have := cptOF (K `&` closure C) B cptKC oB fKB. exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). - split. + split. - by apply: (ctsf) => //; rewrite /filter_of -nbhs_entourageE; exists E'. - - exact: cptOF. - - case=> z h /= [Cz KB Kz]. + - exact: cptOF. + - case=> z h /= [Cz KB Kz]. case: (KB (h z)); first by (exists z; split => //; apply: subset_closure). move=> w [Kw Cw /interior_subset Jfwhz]; apply:subset_split_ent => //. exists (f w); last apply:(near (small_ent_sub _) E') => //. apply: subset_split_ent => //; exists (f u). apply entourage_sym; apply:(near (small_ent_sub _) E') => //. - have [] := Cw (f@^-1` (to_set E' (f w))). + have [] := Cw (f@^-1` (to_set E' (f w))). by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r). by apply:(near (small_ent_sub _) E') => //. @@ -8401,7 +8395,7 @@ move=> W; wlog Wf : f W / W f. by apply: (filterS _ FW) => z Wz; apply: subset_closure. move=> FW ectsW; split=> [ptwsF|]; last exact: pointwise_cvg_compact_family. apply/fam_cvgP => K ? U /=; rewrite uniform_nbhs => [[E [eE EsubU]]]. -suff : \forall g \near within W (nbhs (f : {ptws X -> Y})), +suff : \forall g \near within W (nbhs (f : {ptws X -> Y})), forall y, K y -> E (f y, g y). rewrite near_withinE; near_simpl => N; apply: (filter_app _ _ FW). by apply: ptwsF; near=> g => ?; apply: EsubU; apply: (near N g). @@ -8509,37 +8503,34 @@ Qed. End ArzelaAscoli. +Lemma uniform_regular {T : uniformType} : @regular T. +Proof. +move=> x R; rewrite /= -{1}nbhs_entourageE; case=> E entE ER. +pose E' := (split_ent E); have ? : entourage E' by exact: entourage_split_ent. +exists (to_set (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). + rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. + exact: filterI. +move=> y /= [[? ?]] [? ?]; exists y => //. +Qed. + +#[global] Hint Resolve uniform_regular : core. + Section currying. -Local Notation "U '~>' V" := - ({compact-open, [topologicalType of U] -> [topologicalType of V]}) +Local Notation "U '~>' V" := + ({compact-open, [topologicalType of U] -> [topologicalType of V]}) (at level 99, right associativity). Context {U V W : topologicalType}. -(* -Lemma continuous_snd (f : U ~> V ~> W) (v : V) : - continuous f -> - (forall u, continuous (f u)) -> - continuous (fun (q : U) => f q v). -Proof. -move=> ctsf ctsfp x R /= fxvR; rewrite nbhs_simpl /=. -near=> z => /=; near: z. -have nvE' : nbhs v (f x @^-1` (to_set E' (f x v))). - by apply: ctsfp; rewrite /= -nbhs_entourageE; exists E'. -suff [O Ofx OE] : exists2 O, nbhs (f x) O & (forall g, O g -> E (f x v, g v)). - move/ctsf: Ofx; rewrite /= nbhs_simpl /=; apply: filter_app. - by near_simpl; near=> z => foz; apply: OE. -exists [set g | forall z, [set v] z -> E (f x z, g z)]. - by apply: fam_nbhs => //; exact: compact_set1. -by move=> g; apply. -Unshelve. all: by end_near. Qed. -*) - -Lemma continuous_curry (f : U * V ~> W) : +Lemma continuous_curry (f : U * V ~> W) : continuous f -> continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)) f). Proof. move=> ctsf x; apply/compact_open_cvgP => K O /= cptK oO fKO. -near=> z => /= w /= [+ + <-]; near: z. +near=> z => /= w /= [+ + <-]; near: z. move/compact_near_coveringP/near_covering_withinP: cptK; apply. move=> v Kv; have [[P Q] [Px Qv] PQfO]: nbhs (x,v) (f@^-1` O). by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. @@ -8560,12 +8551,12 @@ have [R Rv RO] : exists2 R, nbhs v R & (forall z, closure R z -> O (f u z)). have [] := reg v ((f u)@^-1` O); first by apply: ctsfp; exact: open_nbhs_nbhs. by move=> R nR cRO; exists R. exists (f @^-1` ([set g | g @` (B `&` closure R) `<=` O]), (B `&` closure R)). - split; [apply/ctsf/open_nbhs_nbhs; split | apply: filterI]. - - apply: compact_open_open => //; apply: compact_closedI => //. + split; [apply/ctsf/open_nbhs_nbhs; split | apply: filterI]. + - apply: compact_open_open => //; apply: compact_closedI => //. exact: closed_closure. - by move=> ? [x [? + <-]]; apply: RO. - done. - - by apply: filterS; [exact: subset_closure|]. + - by apply: filterS; [exact: subset_closure|]. by case=> a r /= [fBMO [Br] cmR]; apply: fBMO; exists r. Qed. @@ -8583,111 +8574,90 @@ Qed. Lemma curry_continuous (f : U * V ~> W) : continuous f -> + @regular U -> {for f, continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)))}. Proof. -move=> ctsf; apply/cvg_sup. - by apply: fmap_filter; apply:nbhs_filter. -case=> K cptK T [C1 [[C2 oR <- Rxcf RT]]]. -move: oR; rewrite openE => /(_ _ Rxcf); case => C3 [E entE] EE' EKR. -move: entE => [O []] => D dcpt <- IDE; rewrite nbhs_simpl /=. -near=> z; apply/RT/EKR/EE'; case=> w Kiw; have Kw : K w by rewrite inE in Kiw. -apply: IDE; rewrite /= /set_val /= /eqincl /incl. -move: w Kw {Kiw C1 C2 Rxcf RT EKR C3 EE' O T}; near: z. -near_simpl; move/compact_near_coveringP/near_covering_withinP : (cptK). -move=> /(_ _ (nbhs f)); apply => u Ku. -apply: filter_bigI_within; (do 3 case) => J cptJ L /[dup] /asboolP entL ? _. -case: entL => C1 [R entR] RC1 C1L. -exists (setT, [set g | forall pq, (K `*` J) pq -> R (f pq, g pq)]). - split; last apply: fam_nbhs => //; last exact: compact_setM. - apply: filterT. -case=> a g /= [? pJR] Ka. -apply: C1L; apply: RC1; rewrite /map_pair; case=> v /= Jiv. -rewrite /= /set_val /= /eqincl /incl. -by apply: pJR; split => //; rewrite inE in Jiv. +move=> ctsf regU; apply/compact_open_cvgP. + by apply: fmap_filter; exact:nbhs_filter. +move=> K ? cptK [D OfinIo <-] fKD /=; near=> z => w [+ + <-]; near: z. +move/compact_near_coveringP/near_covering_withinP : (cptK); apply => u Ku. +have [] := fKD (curry f u); first by exists u. +move=> E /[dup]/[swap]/OfinIo [N Asub <- DIN INf]. +suff : \forall x' \near u & i \near nbhs f, K x' -> + (\bigcap_(i in [set` N]) i) (curry i x'). + apply: filter_app; near=> a b => + Ka => /(_ Ka) => ?. + by exists (\bigcap_(i in [set` N]) i). +apply: filter_bigI_within=> R RN. +have /set_mem [[M cptM _]] := Asub _ RN. +have Rfu : R (curry f u) by exact: INf. +case/(_ _ Rfu) => O [fMO oO] MOR. +near=> p => /= Ki; apply: MOR => + [+ + <-] => _. +move=> v Mv; move: v Mv Ki; near: p. +have umb : \forall y \near u, (forall b, M b -> nbhs (y, b) (f@^-1` O) ). + move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. + have [[P Q] [Pu Qv] PQO] : nbhs (u,v) (f@^-1` O). + by apply: ctsf; apply: open_nbhs_nbhs; split => //; apply: fMO; exists v. + exists (Q, P); [by split| case => b a [Qb Pa Mb]]. + by apply: ctsf; apply: open_nbhs_nbhs; split => //; apply: PQO. +move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. +have [P' P'u cPO] := regU u _ umb. +pose L := [set h | h @`((K `&` (closure P'))`*`M) `<=` O]. +exists (setT, (P' `*` L)). + split => //; first exact: filterT. + exists (P', L) => //; split => //. + apply: open_nbhs_nbhs; split; first apply: compact_open_open => //. + apply: compact_setM => //; apply: compact_closedI => //; exact: closed_closure. + by move=> ? [[a b] [[Ka /cPO +] Mb <-]] => /(_ _ Mb)/nbhs_singleton. +case => b [a h] [? [Pa] +] Ma Ka; apply. +exists (a,b); split => //; split => //; apply/subset_closure => //. Unshelve. all: by end_near. Qed. -Lemma uncurry_continuous (f : U ~> V ~> W) : +Lemma uncurry_continuous (f : U ~> V ~> W) : locally_compact [set: V] -> + @regular V -> + @regular U -> continuous f -> (forall u, continuous (f u)) -> {for f, continuous ((uncurry : (U ~> V ~> W) -> (U * V ~> W)))}. Proof. -move=> lcV ctsf ctsfp; apply/cvg_sup. - by apply: fmap_filter; apply:nbhs_filter. -case=> K cptK T [C1 [[C2 oR <- Rxcf RT]]]. -move: oR; rewrite openE => /(_ _ Rxcf); case => C3 [E entE] EE' EKR. -rewrite nbhs_simpl /=. -near=> z; apply/RT/EKR/EE'; case=> w Kiw; have Kw : K w by rewrite inE in Kiw. -rewrite /= /set_val /= /eqincl /incl. -move: w Kw {Kiw C1 C2 Rxcf RT EKR C3 EE' T}; near: z. -near_simpl; move/compact_near_coveringP/near_covering_withinP : (cptK). -near (powerset_filter_from (@entourage W)) => E'. -have entE' : entourage E' by exact: (near (near_small_set _)). -move=> /(_ _ (nbhs f)); apply; case => u v Kxy. -have ectsf : equicontinuous (f @` (fst @` K)) id. - apply: compact_equicontinuous => //. - by move=> ? [? [? ? <- <-]]; apply: ctsfp. - apply: continuous_compact; first exact: continuous_subspaceT. - apply: continuous_compact => //; apply: continuous_subspaceT => ?; exact: cvg_fst. -have Efv : forall b, \forall y \near b, forall a, (fst @` K) a -> E' (f a b, f a y). - move=> b; move: (ectsf b E' entE'). - apply: filter_app; near=> z => + a [[? r /[swap] /= ->] Kab]. - by apply; exists a => //; exists (a,r). -have cptK2 : compact (snd @` K). - apply: continuous_compact => //; apply: continuous_subspaceT => ?; exact: cvg_snd. -have : \forall y \near v, forall b, (snd @` K) b -> (forall a, (fst @` K) a -> E' (f a b, f a y)). - move/compact_near_coveringP/near_covering_withinP: cptK2. - apply=> // z K2z; have := Efv z E' entE'. - -exists ( - (((f^~ v) @^-1` to_set E' (f u v)) `*` - [set y | forall b, (fst @` K) b -> E' (f b v, f b y)]), - [set g | forall ab, K ab -> E' (f u v, g ab.1 ab.2)]); first last. - case; case => /= a b g [[fvE' P1b] fgE'] Kab. - apply: subset_split_ent => //; exists (f a v) => /=. - apply/entourage_sym; apply: (near (small_ent_sub _) E') => //; apply: P1b. - by exists (a,b). - apply: subset_split_ent => //; exists (f u v) => /=. - apply/entourage_sym; apply: (near (small_ent_sub _) E') => //; apply: fvE'. - by apply: (near (small_ent_sub _) E') => //; apply: (fgE' (a,b)). -split; first exists - (((f^~ v) @^-1` to_set E' (f u v)), - [set y | forall b, (fst @` K) b -> E' (f b v, f b y)]) => //=. - split => //; apply: continuous_snd => //; rewrite /= -nbhs_entourageE. - by exists E'. -rewrite nbhs_simpl /=. - - exists (((f^~ v) @^-1` to_set E' (f u v)), P1) => //; split => //. - by apply: continuous_snd => //=. -rewrite nbhs_simpl /=. -suff : [set g | forall a, (fst @` K) a -> N (f a, g a) ]`<=` - [set g | forall a b, K (a , b) -> E'(f u v, g a b) ]. - move/filterS; apply; apply: fam_nbhs => //; apply: continuous_compact => //. - by apply: continuous_subspaceT => ?; exact: cvg_fst. -move=> g /= fa a b Kab. -apply: fa. -have : nbhs f [set g | forall a b, (fst @` K) -> ] - - - - -have := P1b (g a). -case. -move: P1b; rewrite /P1 (g a). -have := Evcts. - -have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. -have fzE : forall z, nbhs (f z) [set g | forall w, B w -> E (f z w, g w)]. - move=> z; apply: fam_nbhs => //. -move: (fzE u); rewrite -nbhs_entourageE; case=> R entR RBE. -have fE : nbhs f [set g | forall w, (fst @` K) w -> R (f w, g w)]. - apply: fam_nbhs=>//; - by apply: continuous_subspaceT => ?; apply: cvg_fst. -exists ((setT `*` B), [set g | forall w, (fst @` K) w -> R (f w, g w)]). - split => //; exists (setT, B) => //; split => //; exact: filterT. -case;case=> a b /= g [[_ Bb] wKR] KAB. -have /= := (RBE (f a)). -have : nbhs f [set g | forall z, fst @` K z -> ] - - -End currying. \ No newline at end of file +move=> lcV regV regU ctsf ctsfp; apply/compact_open_cvgP. + by apply: fmap_filter; exact:nbhs_filter. +move=> /= K O cptK oO fKO; near=> h => /= ? [+ + <-]; near: h. +move/compact_near_coveringP/near_covering_withinP : (cptK); apply. +case=> u v Kuv. +have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. + have : continuous (uncurry f) by apply: continuous_uncurry_regular. + move/continuousP/(_ _ oO); rewrite openE => /(_ (u,v)) []. + by apply: fKO; exists (u,v). + case=> /= P' Q' [P'u Q'v] PQO. + have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. + have [P Pu cPP'] := regU u P' P'u. + have [Q Qv cQQ'] := regV v Q' Q'v. + exists (closure P), (B `&` closure Q); split. + - exact: closed_closure. + - by apply: compact_closedI => //; exact: closed_closure. + - by apply: filterS; first exact: subset_closure. + - by apply: filterI=> //; apply: filterS; first exact: subset_closure. + - by case => a b [/cPP' ?] [_ /cQQ' ?]; exact: PQO. +case=> P [Q [clP cptQ Pu Qv PQfO]]. +pose R := [set g : V ~> W | g @` Q `<=` O]. +have oR : open R by exact: compact_open_open. +pose P' := f@^-1` R. +pose L := [set h : U ~> V ~> W | h @` (fst @` K `&` P) `<=` R]. +exists (((P`&` P') `*` Q), L). + split => /=. + exists (P `&` P', Q) => //; split => //=; apply: filterI => //. + apply: ctsf; apply: open_nbhs_nbhs; split => // ? [b ? <-]. + by apply: (PQfO (u,b)); split => //; exact: nbhs_singleton. + rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. + apply: compact_open_open => //; apply: compact_closedI => //. + apply: continuous_compact => //; apply: continuous_subspaceT => ?. + exact: cvg_fst. + move=> /= ? [a [Pa ?] <-] ? [b Qb <-]. + by apply: (PQfO (a,b)); split => //; apply: nbhs_singleton. +case; case => a b h [/= [[Pa P'a] Bb Lh] Kab]. +move/(_ (h a)): Lh ; rewrite /L/=/R/=. +apply; first by exists a => //; split => //; exists (a,b). +by exists b. +Unshelve. all: by end_near. Qed. +End currying. From 443ac477d3dd3a9fc592c1619d7ea967d611be3c Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 14 May 2023 21:58:04 -0400 Subject: [PATCH 10/15] needs more linting --- theories/topology.v | 146 +++++++++++++++++++------------------------- 1 file changed, 63 insertions(+), 83 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 9aa18fd2f0..315dd99213 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -6725,14 +6725,14 @@ Unshelve. all: by end_near. Qed. (* It turns out {family compact, U -> V} can be generalized to only assume *) (* `topologicalType` on V. This topology is called the compact-open topology. *) -(* This topology is special becaise its the _only_ topology that will allow *) +(* This topology is special becaise it _only_ topology that will allow *) (* curry/uncurry to be continuous. *) Section compact_open. Context {T U : topologicalType}. -Definition compact_open := (T->U)^o. +Definition compact_open : Type := T->U. Section compact_open_setwise. Context {K : set T}. @@ -6801,7 +6801,7 @@ Qed. Lemma compact_open_open (K : set T) (O : set U) : compact K -> open O -> open ([set g | g @` K `<=` O] : set compact_open). Proof. -pose C := [set g | g @` K `<=` O]; move=> cptK oO. +pose C := [set g | g @` K `<=` O]; move=> cptK oO. exists [set C]; last by rewrite bigcup_set1. move=> ? ->; exists (fset1 C) => //; last by rewrite set_fset1 bigcap_set1. by move=> ?; rewrite ?inE => ->; exists (existT _ _ cptK) => // z Cz; exists O. @@ -6831,43 +6831,41 @@ Lemma compact_open_fam_compactP (f : U -> V) (F : set (set (U -> V))) : continuous f -> (Filter F) -> {compact-open, F --> f} <-> {family compact, F --> f}. Proof. -move=> ctsf FF; split. - move/compact_open_cvgP=> cptOF; apply/cvg_sup; case=> K cptK R. - case=> D /= [[E oE <- /=] Ekf] /filterS; apply. - move: oE; rewrite openE => /(_ _ Ekf); case => ? [J entJ /=] EKR KfE. - near=> z; apply/KfE/EKR; case => u /= Kp. - rewrite /= /set_val /= /eqincl /incl/set_val /= /comp. - (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))%classic. - pose B := \bigcup_(z in K `&` closure C) interior (to_set E' (f z)). - have oB : open B by apply: bigcup_open => ? ?; exact: open_interior. - have fKB : f @` (K `&` closure C) `<=` B. - move=> ? [z ? <-]; exists z => //; rewrite /interior. - by rewrite -nbhs_entourageE; exists E'. - have cptKC : compact (K `&` closure C). - apply: compact_closedI => //; exact: closed_closure. - have := cptOF (K `&` closure C) B cptKC oB fKB. - exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). - split. - - by apply: (ctsf) => //; rewrite /filter_of -nbhs_entourageE; exists E'. - - exact: cptOF. - - case=> z h /= [Cz KB Kz]. - case: (KB (h z)); first by (exists z; split => //; apply: subset_closure). - move=> w [Kw Cw /interior_subset Jfwhz]; apply:subset_split_ent => //. - exists (f w); last apply:(near (small_ent_sub _) E') => //. - apply: subset_split_ent => //; exists (f u). - apply entourage_sym; apply:(near (small_ent_sub _) E') => //. - have [] := Cw (f@^-1` (to_set E' (f w))). - by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. - move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r). - by apply:(near (small_ent_sub _) E') => //. - by apply entourage_sym; apply:(near (small_ent_sub _) E') => //. -move=> cptF; apply/compact_open_cvgP => K O cptK oO fKO. -apply: cptF; have := fam_compact_nbhs oO fKO cptK ctsf; apply: filter_app. -by near=> g => /= gKO ? [z Kx <-]; apply: gKO. +move=> ctsf FF; split; first last. + move=> cptF; apply/compact_open_cvgP => K O cptK oO fKO. + apply: cptF; have := fam_compact_nbhs oO fKO cptK ctsf; apply: filter_app. + by near=> g => /= gKO ? [z Kx <-]; apply: gKO. +move/compact_open_cvgP=> cptOF; apply/cvg_sup; case=> K cptK R. +case=> D [[E oE <-] Ekf] /filterS; apply. +move: oE; rewrite openE => /(_ _ Ekf); case => ? [J entJ] EKR KfE. +near=> z; apply/KfE/EKR; case => u Kp; rewrite /= /set_val /= /eqincl /incl. +(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)). +have oB : open B by apply: bigcup_open => ? ?; exact: open_interior. +have fKB : f @` (K `&` closure C) `<=` B. + move=> ? [z ? <-]; exists z => //; rewrite /interior. + by rewrite -nbhs_entourageE; exists E'. +have cptKC : compact (K `&` closure C). + by apply: compact_closedI => //; exact: closed_closure. +have := cptOF (K `&` closure C) B cptKC oB fKB. +exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). + split; last exact: cptOF. + by apply: (ctsf) => //; rewrite /filter_of -nbhs_entourageE; exists E'. +case=> z h /= [Cz KB Kz]. +case: (KB (h z)); first by (exists z; split => //; apply: subset_closure). +move=> w [Kw Cw /interior_subset Jfwhz]; apply:subset_split_ent => //. +exists (f w); last apply:(near (small_ent_sub _) E') => //. +apply: subset_split_ent => //; exists (f u). + apply entourage_sym; apply:(near (small_ent_sub _) E') => //. +have [] := Cw (f@^-1` (to_set E' (f w))). + by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. +move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r). + by apply:(near (small_ent_sub _) E') => //. +by apply entourage_sym; apply:(near (small_ent_sub _) E') => //. Unshelve. all: by end_near. Qed. End compact_open_uniform. @@ -8527,10 +8525,10 @@ Local Notation "U '~>' V" := Context {U V W : topologicalType}. Lemma continuous_curry (f : U * V ~> W) : - continuous f -> continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)) f). + continuous f -> continuous (curry f : (U ~> V ~> W)). Proof. move=> ctsf x; apply/compact_open_cvgP => K O /= cptK oO fKO. -near=> z => /= w /= [+ + <-]; near: z. +near=> z => w /= [+ + <-]; near: z. move/compact_near_coveringP/near_covering_withinP: cptK; apply. move=> v Kv; have [[P Q] [Px Qv] PQfO]: nbhs (x,v) (f@^-1` O). by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. @@ -8538,32 +8536,25 @@ by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; apply: PQfO. Unshelve. all: by end_near. Qed. Lemma continuous_uncurry_regular (f : U ~> V ~> W): - locally_compact [set: V] -> - @regular V -> - continuous f -> - (forall u, continuous (f u)) -> - continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). + locally_compact [set: V] -> @regular V -> continuous f -> + (forall u, continuous (f u)) -> continuous (uncurry f : ((U * V) ~> W)). Proof. -move=> lcV reg ctsf ctsfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv]. -move/filterS; apply. -have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. +move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv] /filterS. +apply; have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. have [R Rv RO] : exists2 R, nbhs v R & (forall z, closure R z -> O (f u z)). - have [] := reg v ((f u)@^-1` O); first by apply: ctsfp; exact: open_nbhs_nbhs. - by move=> R nR cRO; exists R. + have [] := reg v ((f u)@^-1` O); first by apply: cfp; exact: open_nbhs_nbhs. + by move=> R ? ?; exists R. exists (f @^-1` ([set g | g @` (B `&` closure R) `<=` O]), (B `&` closure R)). - split; [apply/ctsf/open_nbhs_nbhs; split | apply: filterI]. + split; [apply/cf/open_nbhs_nbhs; split | apply: filterI] => //. - apply: compact_open_open => //; apply: compact_closedI => //. exact: closed_closure. - by move=> ? [x [? + <-]]; apply: RO. - - done. - by apply: filterS; [exact: subset_closure|]. by case=> a r /= [fBMO [Br] cmR]; apply: fBMO; exists r. Qed. Lemma continuous_uncurry (f : U ~> V ~> W): - locally_compact [set: V] -> - hausdorff_space V -> - continuous f -> + locally_compact [set: V] -> hausdorff_space V -> continuous f -> (forall u, continuous (f u)) -> continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). Proof. @@ -8572,9 +8563,7 @@ move=> v; have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. by move=> z; apply: (@compact_regular V hsdf v B). Qed. -Lemma curry_continuous (f : U * V ~> W) : - continuous f -> - @regular U -> +Lemma curry_continuous (f : U * V ~> W) : continuous f -> @regular U -> {for f, continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)))}. Proof. move=> ctsf regU; apply/compact_open_cvgP. @@ -8587,12 +8576,10 @@ suff : \forall x' \near u & i \near nbhs f, K x' -> (\bigcap_(i in [set` N]) i) (curry i x'). apply: filter_app; near=> a b => + Ka => /(_ Ka) => ?. by exists (\bigcap_(i in [set` N]) i). -apply: filter_bigI_within=> R RN. -have /set_mem [[M cptM _]] := Asub _ RN. +apply: filter_bigI_within=> R RN; have /set_mem [[M cptM _]] := Asub _ RN. have Rfu : R (curry f u) by exact: INf. -case/(_ _ Rfu) => O [fMO oO] MOR. -near=> p => /= Ki; apply: MOR => + [+ + <-] => _. -move=> v Mv; move: v Mv Ki; near: p. +case/(_ _ Rfu) => O [fMO oO] MOR; near=> p => /= Ki; apply: MOR => + [+ + <-]. +move=> _ v Mv; move: v Mv Ki; near: p. have umb : \forall y \near u, (forall b, M b -> nbhs (y, b) (f@^-1` O) ). move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. have [[P Q] [Pu Qv] PQO] : nbhs (u,v) (f@^-1` O). @@ -8603,26 +8590,23 @@ move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. have [P' P'u cPO] := regU u _ umb. pose L := [set h | h @`((K `&` (closure P'))`*`M) `<=` O]. exists (setT, (P' `*` L)). - split => //; first exact: filterT. - exists (P', L) => //; split => //. + split => //; [exact: filterT|]; exists (P', L) => //; split => //. apply: open_nbhs_nbhs; split; first apply: compact_open_open => //. - apply: compact_setM => //; apply: compact_closedI => //; exact: closed_closure. + apply: compact_setM => //; apply: compact_closedI => //. + exact: closed_closure. by move=> ? [[a b] [[Ka /cPO +] Mb <-]] => /(_ _ Mb)/nbhs_singleton. case => b [a h] [? [Pa] +] Ma Ka; apply. exists (a,b); split => //; split => //; apply/subset_closure => //. Unshelve. all: by end_near. Qed. Lemma uncurry_continuous (f : U ~> V ~> W) : - locally_compact [set: V] -> - @regular V -> - @regular U -> - continuous f -> - (forall u, continuous (f u)) -> + locally_compact [set: V] -> @regular V -> @regular U -> + continuous f -> (forall u, continuous (f u)) -> {for f, continuous ((uncurry : (U ~> V ~> W) -> (U * V ~> W)))}. Proof. move=> lcV regV regU ctsf ctsfp; apply/compact_open_cvgP. by apply: fmap_filter; exact:nbhs_filter. -move=> /= K O cptK oO fKO; near=> h => /= ? [+ + <-]; near: h. +move=> /= K O cptK oO fKO; near=> h => ? [+ + <-]; near: h. move/compact_near_coveringP/near_covering_withinP : (cptK); apply. case=> u v Kuv. have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. @@ -8631,18 +8615,15 @@ have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` un by apply: fKO; exists (u,v). case=> /= P' Q' [P'u Q'v] PQO. have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. - have [P Pu cPP'] := regU u P' P'u. - have [Q Qv cQQ'] := regV v Q' Q'v. + have [P Pu cPP'] := regU u P' P'u; have [Q Qv cQQ'] := regV v Q' Q'v. exists (closure P), (B `&` closure Q); split. - exact: closed_closure. - by apply: compact_closedI => //; exact: closed_closure. - by apply: filterS; first exact: subset_closure. - by apply: filterI=> //; apply: filterS; first exact: subset_closure. - by case => a b [/cPP' ?] [_ /cQQ' ?]; exact: PQO. -case=> P [Q [clP cptQ Pu Qv PQfO]]. -pose R := [set g : V ~> W | g @` Q `<=` O]. -have oR : open R by exact: compact_open_open. -pose P' := f@^-1` R. +case=> P [Q [clP cptQ Pu Qv PQfO]]; pose R := [set g : V ~> W | g @` Q `<=` O]. +(have oR : open R by exact: compact_open_open); pose P' := f@^-1` R. pose L := [set h : U ~> V ~> W | h @` (fst @` K `&` P) `<=` R]. exists (((P`&` P') `*` Q), L). split => /=. @@ -8655,9 +8636,8 @@ exists (((P`&` P') `*` Q), L). exact: cvg_fst. move=> /= ? [a [Pa ?] <-] ? [b Qb <-]. by apply: (PQfO (a,b)); split => //; apply: nbhs_singleton. -case; case => a b h [/= [[Pa P'a] Bb Lh] Kab]. -move/(_ (h a)): Lh ; rewrite /L/=/R/=. -apply; first by exists a => //; split => //; exists (a,b). +case; case => a b h [/= [[? ?] ? Lh] ?]. +apply: (Lh (h a)); first by exists a => //; split => //; exists (a,b). by exists b. Unshelve. all: by end_near. Qed. End currying. From bfeadac1a48a9a82fb0c77bd13ab9da48fdb2915 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 28 Dec 2023 18:19:13 -0500 Subject: [PATCH 11/15] linting and comments --- theories/topology.v | 107 +++++++++++++++++++++++++------------------- 1 file changed, 60 insertions(+), 47 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 315dd99213..3c634851a5 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1727,30 +1727,30 @@ Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set (set T)) Proof. move=> FF [] G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from F). - by apply: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. near=> M; apply: GP; apply: (Gs D) => //. apply: filterS; first exact: preimage_image. - by apply: (near (near_small_set _) M). -have : M `<=` f @^-1` D by apply: (near (small_set_sub FfD) M). -by move/image_subset/subset_trans; apply; apply: image_preimage_subset. + exact: (near (near_small_set _) M). +have : M `<=` f @^-1` D by exact: (near (small_set_sub FfD) M). +by move/image_subset/subset_trans; apply; exact: image_preimage_subset. Unshelve. all: by end_near. Qed. -Lemma near_map_powerset {T U : Type} (f : T -> U) (F : set (set T)) +Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set (set T)) (P : (set U) -> Prop) : (forall X Y, X `<=` Y -> P Y -> P X) -> ProperFilter F -> - (\forall y \near powerset_filter_from F, P (f @` y)) -> + (\forall y \near powerset_filter_from F, P (f @` y)) = (\forall y \near powerset_filter_from (f x @[x --> F]), P y). Proof. -move=> Psub FF [] G /= [Gf Gs [D GD GP]]. +move=> Pmono FF; rewrite propeqE; split; last exact: near_powerset_map. +case=> G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). - by apply: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. -have ffiD : fmap f F (f@` D). + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D). by rewrite /fmap /=; apply: filterS; first exact: preimage_image. -near=> M; have FfM : (fmap f F M) by apply (near (near_small_set _) M). -apply: (@Psub _ (f@`D)); first exact: (near (small_set_sub ffiD) M). +near=> M; have FfM : (fmap f F M) by exact: (near (near_small_set _) M). +apply: (@Pmono _ (f@`D)); first exact: (near (small_set_sub ffiD) M). exact: GP. Unshelve. all: by end_near. Qed. @@ -2542,8 +2542,7 @@ Lemma fst_open {U V : topologicalType} (A : set (U * V)) : Proof. rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. have [[P Q] [Pa ?] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => //. -move=> p Pp; exists (p, b) => //; apply: pqA; split => //. -exact: nbhs_singleton. +by move=> p ?; exists (p, b); [apply: pqA; split|]; [|exact: nbhs_singleton|]. Qed. Lemma snd_open {U V : topologicalType} (A : set (U * V)) : @@ -3153,17 +3152,10 @@ Definition near_covering_within (K : set X) := Lemma near_covering_withinP (K : set X): near_covering_within K <-> near_covering K. Proof. -split. - move=> cvrW I F P FF cvr. - near=> i; suff : K `<=` (fun q : X => K q -> P i q). - by move=> KKP k Kk; apply: KKP. - near: i; apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app. - by near=> j => /=. -move=> cvrW I F P FF cvr. -near=> i; suff : K `<=` (fun q : X => K q -> P i q). - by move=> KKP k Kk; apply: KKP. -near: i. -have := (cvrW I F (fun i q => K q -> P i q) FF). +split; move=> cvrW I F P FF cvr; near=> i; + (suff : K `<=` fun q : X => K q -> P i q by move=> + k Kk; apply); near: i. + by apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app; near=> j. +have := (cvrW _ _ (fun i q => K q -> P i q) FF). apply => x Kx; have := cvr x Kx; apply: filter_app. by near=> j => + ?; apply. Unshelve. all: by end_near. Qed. @@ -3177,12 +3169,11 @@ rewrite ?compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. have := cptP I F (fun i u => forall q, Q q -> Pr i (u,q)) Ff. set R := (R in (R -> _) -> _); suff R' : R. by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. -rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)). -move=> v Qv. +rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)) => v Qv. case: (cvfPQ (x,v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. exists (N2,(N1`*`G)); first by split => //; exists (N1, G) => //. case=> a [b i] /= [? [?]] ?. -by apply: (ngPr (b,a, i)); split => //; apply: N1N2N. +by apply: (ngPr (b,a, i)); split => //; exact: N1N2N. Unshelve. all: by end_near. Qed. Section Tychonoff. @@ -6725,7 +6716,7 @@ Unshelve. all: by end_near. Qed. (* It turns out {family compact, U -> V} can be generalized to only assume *) (* `topologicalType` on V. This topology is called the compact-open topology. *) -(* This topology is special becaise it _only_ topology that will allow *) +(* This topology is special becaise it is the _only_ topology that will allow *) (* curry/uncurry to be continuous. *) Section compact_open. @@ -6752,7 +6743,7 @@ apply: filter_from_filter; first by exists setT; split => //; exact: openT. move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split. - by move=> ? [z Kz M-]; split; [apply: fKP | apply: fKQ]; exists z. - exact: openI. -by move=> g /= gPQ; split; apply: (subset_trans gPQ) => ? []. +by move=> g /= gPQ; split; exact: (subset_trans gPQ) => ? []. Qed. Program Definition compact_openK_topological_mixin : @@ -6763,7 +6754,7 @@ Next Obligation. move=> f; rewrite eqEsubset; split => A /=. case=> B /= [fKB oB gKBA]; exists [set g | g @` K `<=` B]; split => //. by move=> h /= hKB; exists B. -by case=> B [oB Bf /filterS]; apply; apply: oB. +by case=> B [oB Bf /filterS]; apply; exact: oB. Qed. Next Obligation. done. Qed. @@ -8512,7 +8503,7 @@ move=> z /= clEz; apply: ER; apply: subset_split_ent => //. have [] := clEz (to_set (E' `&` E'^-1%classic) z). rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. exact: filterI. -move=> y /= [[? ?]] [? ?]; exists y => //. +by move=> y /= [[? ?]] [? ?]; exists y. Qed. #[global] Hint Resolve uniform_regular : core. @@ -8522,17 +8513,39 @@ Local Notation "U '~>' V" := ({compact-open, [topologicalType of U] -> [topologicalType of V]}) (at level 99, right associativity). +Section cartesian_closed. Context {U V W : topologicalType}. +(* In this section, we consider under what conditions + [f in U ~> V ~> W | continuous f /\ forall u, continuous (f u)] + and + [f in U * V ~> W | continuous f] + are homeomorphic + - Always: + curry sends cts functions to cts functions + - V locally_compact + regular or hausdorff + uncurry sends cts functions to cts functions + - U regular or hausdorff + curry itself is a continuous map + - U regular or hausdorff AND V locally_compact + regular or hausdorff + uncurry itself is a continuous map + Therefore curry/uncurry are homeomorphisms + So the category of locally compact regular spaces is cartesian closed +*) + Lemma continuous_curry (f : U * V ~> W) : - continuous f -> continuous (curry f : (U ~> V ~> W)). + continuous f -> + continuous (curry f : (U ~> V ~> W)) /\ forall u, continuous (curry f u). Proof. -move=> ctsf x; apply/compact_open_cvgP => K O /= cptK oO fKO. +move=> ctsf; split; first last. + move=> u z; apply: continuous_comp; last exact: ctsf. + by apply: cvg_pair => //=; exact: cvg_cst. +move=> x; apply/compact_open_cvgP => K O /= cptK oO fKO. near=> z => w /= [+ + <-]; near: z. move/compact_near_coveringP/near_covering_withinP: cptK; apply. move=> v Kv; have [[P Q] [Px Qv] PQfO]: nbhs (x,v) (f@^-1` O). by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. -by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; apply: PQfO. +by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; exact: PQfO. Unshelve. all: by end_near. Qed. Lemma continuous_uncurry_regular (f : U ~> V ~> W): @@ -8541,7 +8554,7 @@ Lemma continuous_uncurry_regular (f : U ~> V ~> W): Proof. move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv] /filterS. apply; have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. -have [R Rv RO] : exists2 R, nbhs v R & (forall z, closure R z -> O (f u z)). +have [R Rv RO] : exists2 R, nbhs v R & forall z, closure R z -> O (f u z). have [] := reg v ((f u)@^-1` O); first by apply: cfp; exact: open_nbhs_nbhs. by move=> R ? ?; exists R. exists (f @^-1` ([set g | g @` (B `&` closure R) `<=` O]), (B `&` closure R)). @@ -8574,7 +8587,7 @@ have [] := fKD (curry f u); first by exists u. move=> E /[dup]/[swap]/OfinIo [N Asub <- DIN INf]. suff : \forall x' \near u & i \near nbhs f, K x' -> (\bigcap_(i in [set` N]) i) (curry i x'). - apply: filter_app; near=> a b => + Ka => /(_ Ka) => ?. + apply: filter_app; near=> a b => /[apply] ?. by exists (\bigcap_(i in [set` N]) i). apply: filter_bigI_within=> R RN; have /set_mem [[M cptM _]] := Asub _ RN. have Rfu : R (curry f u) by exact: INf. @@ -8607,9 +8620,10 @@ Proof. move=> lcV regV regU ctsf ctsfp; apply/compact_open_cvgP. by apply: fmap_filter; exact:nbhs_filter. move=> /= K O cptK oO fKO; near=> h => ? [+ + <-]; near: h. -move/compact_near_coveringP/near_covering_withinP : (cptK); apply. +move/compact_near_coveringP/near_covering_withinP: (cptK); apply. case=> u v Kuv. -have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. +have : exists P Q, [/\ closed P, compact Q, nbhs u P, + nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. have : continuous (uncurry f) by apply: continuous_uncurry_regular. move/continuousP/(_ _ oO); rewrite openE => /(_ (u,v)) []. by apply: fKO; exists (u,v). @@ -8625,12 +8639,11 @@ have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` un case=> P [Q [clP cptQ Pu Qv PQfO]]; pose R := [set g : V ~> W | g @` Q `<=` O]. (have oR : open R by exact: compact_open_open); pose P' := f@^-1` R. pose L := [set h : U ~> V ~> W | h @` (fst @` K `&` P) `<=` R]. -exists (((P`&` P') `*` Q), L). - split => /=. - exists (P `&` P', Q) => //; split => //=; apply: filterI => //. - apply: ctsf; apply: open_nbhs_nbhs; split => // ? [b ? <-]. - by apply: (PQfO (u,b)); split => //; exact: nbhs_singleton. - rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. +exists (((P`&` P') `*` Q), L); first split => /=. +- exists (P `&` P', Q) => //; split => //=; apply: filterI => //. + apply: ctsf; apply: open_nbhs_nbhs; split => // ? [b ? <-]. + by apply: (PQfO (u,b)); split => //; exact: nbhs_singleton. +- rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. apply: compact_open_open => //; apply: compact_closedI => //. apply: continuous_compact => //; apply: continuous_subspaceT => ?. exact: cvg_fst. @@ -8640,4 +8653,4 @@ case; case => a b h [/= [[? ?] ? Lh] ?]. apply: (Lh (h a)); first by exists a => //; split => //; exists (a,b). by exists b. Unshelve. all: by end_near. Qed. -End currying. +End cartesian_closed. From 9483bf50c345c4d9d66b9c4b1053b3763d093de5 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 28 Dec 2023 20:45:49 -0500 Subject: [PATCH 12/15] closing section --- theories/topology.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/topology.v b/theories/topology.v index 3c634851a5..3f9292715f 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -8654,3 +8654,4 @@ apply: (Lh (h a)); first by exists a => //; split => //; exists (a,b). by exists b. Unshelve. all: by end_near. Qed. End cartesian_closed. +End currying. \ No newline at end of file From c996c416fc151c4731b600e22f122200a1de07f2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 11 Jan 2024 23:35:18 +0900 Subject: [PATCH 13/15] changelog, typo - format doc --- CHANGELOG_UNRELEASED.md | 35 +++++ theories/topology.v | 275 ++++++++++++++++++++-------------------- 2 files changed, 173 insertions(+), 137 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f96118e538..0999ff4e41 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,10 +13,45 @@ - in `lebesgue_integral.v`: + `sigma_finite_measure` instance on product measure `\x` +- in `topology.v`: + + lemma `filter_bigI_within` + + lemma `near_powerset_map` + + lemma `near_powerset_map_monoE` + + lemma `fst_open` + + lemma `snd_open` + + definition `near_covering_within` + + lemma `near_covering_withinP` + + lemma `compact_setM` + + definition `regular` + + lemma `compact_regular` + + lemma `fam_compact_nbhs` + + definition `compact_open`, notation `{compact-open, U -> V}` + + notation `{compact-open, F --> f}` + + definition `compact_openK` + + definition `compact_openK_nbhs` + + instance `compact_openK_nbhs_filter` + + definition `compact_openK_topological_mixin` + + canonicals `compact_openK_filter`, `compact_openK_topological`, + `compact_open_pointedType` + + definition `compact_open_topologicalType` + + canonicals `compact_open_filtered`, `compact_open_topological` + + lemma `compact_open_cvgP` + + lemma `compact_open_open` + + lemma `compact_closedI` + + lemma `compact_open_fam_compactP` + + lemma `compact_equicontinuous` + + lemma `uniform_regular` + + lemma `continuous_curry` + + lemma `continuous_uncurry_regular` + + lemma `continuous_uncurry` + + lemma `curry_continuous` + + lemma `uncurry_continuous` + ### Changed - in `topology.v`: + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}` + + lemma `pointwise_compact_cvg` ### Renamed diff --git a/theories/topology.v b/theories/topology.v index 3f9292715f..d05a8c7165 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1226,7 +1226,7 @@ Qed. Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) (F : set (set T)) : Filter F -> (forall i, i \in D -> F (f i)) -> - F (\bigcap_(i in [set i | i \in D]) f i). + F (\bigcap_(i in [set` D]) f i). Proof. move=> FF FfD. suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. @@ -1630,8 +1630,8 @@ Canonical within_filter_on T D (F : filter_on T) := Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) (F : set (set T)) (P : set T) : - Filter F -> (forall i, i \in D -> F ([set j | P j -> f i j])) -> - F ([set j | P j -> (\bigcap_(i in [set i | i \in D]) f i) j]). + Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> + F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]). Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. Definition subset_filter {T} (F : set (set T)) (D : set T) := @@ -1720,7 +1720,7 @@ Qed. End NearSet. Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set (set T)) - (P : (set U) -> Prop) : + (P : set U -> Prop) : ProperFilter F -> (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> (\forall y \near powerset_filter_from F, P (f @` y)). @@ -1728,7 +1728,7 @@ Proof. move=> FF [] G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from F). exact: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. near=> M; apply: GP; apply: (Gs D) => //. apply: filterS; first exact: preimage_image. exact: (near (near_small_set _) M). @@ -1737,7 +1737,7 @@ by move/image_subset/subset_trans; apply; exact: image_preimage_subset. Unshelve. all: by end_near. Qed. Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set (set T)) - (P : (set U) -> Prop) : + (P : set U -> Prop) : (forall X Y, X `<=` Y -> P Y -> P X) -> ProperFilter F -> (\forall y \near powerset_filter_from F, P (f @` y)) = @@ -1749,8 +1749,8 @@ have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). exact: powerset_filter_from_filter. have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D). by rewrite /fmap /=; apply: filterS; first exact: preimage_image. -near=> M; have FfM : (fmap f F M) by exact: (near (near_small_set _) M). -apply: (@Pmono _ (f@`D)); first exact: (near (small_set_sub ffiD) M). +near=> M; have FfM : fmap f F M by exact: (near (near_small_set _) M). +apply: (@Pmono _ (f @` D)); first exact: (near (small_set_sub ffiD) M). exact: GP. Unshelve. all: by end_near. Qed. @@ -2540,18 +2540,17 @@ End Prod_Topology. Lemma fst_open {U V : topologicalType} (A : set (U * V)) : open A -> open (fst @` A). Proof. -rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. -have [[P Q] [Pa ?] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => //. -by move=> p ?; exists (p, b); [apply: pqA; split|]; [|exact: nbhs_singleton|]. +rewrite !openE => oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [Pa Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => // p Pp. +by exists (p, b) => //=; apply: pqA; split=> //=; exact: nbhs_singleton. Qed. Lemma snd_open {U V : topologicalType} (A : set (U * V)) : open A -> open (snd @` A). Proof. -rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. -have [[P Q] [? Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => //. -move=> q Qq; exists (a, q) => //; apply: pqA; split => //. -exact: nbhs_singleton. +rewrite !openE => oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [Pa Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => // q Qq. +by exists (a, q) => //=; apply: pqA; split => //; exact: nbhs_singleton. Qed. Section matrix_Topology. @@ -3149,15 +3148,14 @@ Definition near_covering_within (K : set X) := (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> \near F, K `<=` P F. -Lemma near_covering_withinP (K : set X): +Lemma near_covering_withinP (K : set X) : near_covering_within K <-> near_covering K. Proof. -split; move=> cvrW I F P FF cvr; near=> i; - (suff : K `<=` fun q : X => K q -> P i q by move=> + k Kk; apply); near: i. - by apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app; near=> j. -have := (cvrW _ _ (fun i q => K q -> P i q) FF). -apply => x Kx; have := cvr x Kx; apply: filter_app. -by near=> j => + ?; apply. +split => cvrW I F P FF cvr; near=> i; + (suff: K `<=` fun q : X => K q -> P i q by move=> + k Kk; exact); near: i. + by apply: cvrW => x /cvr; apply: filter_app; near=> j. +have := cvrW _ _ (fun i q => K q -> P i q) FF. +by apply => x /cvr; apply: filter_app; near=> j => + ?; apply. Unshelve. all: by end_near. Qed. End near_covering. @@ -3165,15 +3163,15 @@ End near_covering. Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) : compact P -> compact Q -> compact (P `*` Q). Proof. -rewrite ?compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. -have := cptP I F (fun i u => forall q, Q q -> Pr i (u,q)) Ff. +rewrite !compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. +have := cptP I F (fun i u => forall q, Q q -> Pr i (u, q)) Ff. set R := (R in (R -> _) -> _); suff R' : R. by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)) => v Qv. -case: (cvfPQ (x,v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. -exists (N2,(N1`*`G)); first by split => //; exists (N1, G) => //. -case=> a [b i] /= [? [?]] ?. -by apply: (ngPr (b,a, i)); split => //; exact: N1N2N. +case: (cvfPQ (x, v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. +exists (N2, N1`*`G); first by split => //; exists (N1, G). +case=> a [b i] /= [N2a [N1b]] Gi. +by apply: (ngPr (b, a, i)); split => //; exact: N1N2N. Unshelve. all: by end_near. Qed. Section Tychonoff. @@ -3648,11 +3646,11 @@ move=> /DsubC /= [y /= yfs hyz]; exists (h' y) => //. by rewrite set_imfset /=; exists y. Qed. -Definition regular {T : topologicalType} := forall (x:T), - (filter_from (nbhs x) closure) --> x. +Definition regular {T : topologicalType} := forall x : T, + filter_from (nbhs x) closure --> x. Section separated_topologicalType. -Variable (T : topologicalType). +Variable T : topologicalType. Implicit Types x y : T. Local Open Scope classical_set_scope. @@ -3819,13 +3817,13 @@ move=> cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //. move=> P Q Px Qx; exists (P `&` Q); [exact: filterI | exact: closureI]. - by exists V => //; have /closure_id <- : closed V by exact: compact_closed. rewrite eqEsubset; split; first last. - move=> ? -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //. + move=> _ -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //. by apply/CA/subset_closure; exact: nbhs_singleton. move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply]. -case; case=> B A /=; rewrite ?inE; case=> By Ax [oB oA BA0]. +move=> [[B A]]/=; rewrite ?inE; case=> By Ax [oB oA BA0]. apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP. -split; first by exists A => //; apply: open_nbhs_nbhs. -apply/not_implyP; split; first by exact: open_nbhs_nbhs. +split; first by exists A => //; exact: open_nbhs_nbhs. +apply/not_implyP; split; first exact: open_nbhs_nbhs. apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset. have /closure_id -> : closed (~` B); first by exact: open_closedC. by apply/closure_subset/disjoints_subset; rewrite setIC. @@ -6698,29 +6696,28 @@ Qed. Lemma fam_compact_nbhs {U : topologicalType} {V : uniformType} (A : set U) (O : set V) (f : {family compact, U -> V}) : - open O -> (f @` A `<=` O) -> compact A -> continuous f -> + open O -> f @` A `<=` O -> compact A -> continuous f -> nbhs (f : {family compact, U -> V}) [set g | forall y, A y -> O (g y)]. Proof. -move=> oO fAO /[dup] ? /compact_near_coveringP/near_covering_withinP cfA ctsf. -near=> z => /=; (suff : A `<=` [set y | O (z y)] by exact); near: z. -apply: cfA => x Ax; have : O (f x) by apply: fAO. +move=> oO fAO /[dup] cA /compact_near_coveringP/near_covering_withinP cfA ctsf. +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; case => E entE EfO. -exists (f @^-1` (to_set (split_ent E) (f x)), +rewrite /interior -nbhs_entourageE => -[E entE EfO]. +exists (f @^-1` to_set (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) => //=; last exact: AEg. +by exists (f y) => //=; exact: AEg. Unshelve. all: by end_near. Qed. (* It turns out {family compact, U -> V} can be generalized to only assume *) (* `topologicalType` on V. This topology is called the compact-open topology. *) -(* This topology is special becaise it is the _only_ topology that will allow *) +(* This topology is special because it is the _only_ topology that will allow *) (* curry/uncurry to be continuous. *) Section compact_open. - Context {T U : topologicalType}. Definition compact_open : Type := T->U. @@ -6733,7 +6730,7 @@ Definition compact_openK := let _ := K in compact_open. Definition compact_openK_nbhs (f : compact_openK) := filter_from [set O | f @` K `<=` O /\ open O] - (fun O => [set g | g @` K `<=` O]). + (fun O => [set g | g @` K `<=` O]). Global Instance compact_openK_nbhs_filter (f : compact_openK) : ProperFilter (compact_openK_nbhs f). @@ -6743,7 +6740,7 @@ apply: filter_from_filter; first by exists setT; split => //; exact: openT. move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split. - by move=> ? [z Kz M-]; split; [apply: fKP | apply: fKQ]; exists z. - exact: openI. -by move=> g /= gPQ; split; exact: (subset_trans gPQ) => ? []. +by move=> g /= gPQ; split; exact: (subset_trans gPQ). Qed. Program Definition compact_openK_topological_mixin : @@ -6756,7 +6753,7 @@ move=> f; rewrite eqEsubset; split => A /=. by move=> h /= hKB; exists B. by case=> B [oB Bf /filterS]; apply; exact: oB. Qed. -Next Obligation. done. Qed. +Next Obligation. by []. Qed. Canonical compact_openK_filter := FilteredType compact_openK compact_openK compact_openK_nbhs. @@ -6780,22 +6777,22 @@ Canonical compact_open_topological := Lemma compact_open_cvgP (F : set (set (compact_open_topological))) (f : compact_open_topological) : Filter F -> - (F --> f) <-> (forall K O, @compact T K -> @open U O -> f @` K `<=` O -> - F [set g | g @` K `<=` O] ). + F --> f <-> forall K O, @compact T K -> @open U O -> f @` K `<=` O -> + F [set g | g @` K `<=` O]. Proof. move=> FF; split. by move/cvg_sup => + K O cptK ? ? => /(_ (existT _ _ cptK)); apply; exists O. -move=> fko; apply/cvg_sup; case=> A cptK O /= [C /= [fAC oC]]. -by move/filterS; apply; apply: fko. +move=> fko; apply/cvg_sup => -[A cptK] O /= [C /= [fAC oC]]. +by move/filterS; apply; exact: fko. Qed. Lemma compact_open_open (K : set T) (O : set U) : compact K -> open O -> open ([set g | g @` K `<=` O] : set compact_open). Proof. -pose C := [set g | g @` K `<=` O]; move=> cptK oO. +pose C := [set g | g @` K `<=` O]; move=> cptK oO. exists [set C]; last by rewrite bigcup_set1. -move=> ? ->; exists (fset1 C) => //; last by rewrite set_fset1 bigcap_set1. -by move=> ?; rewrite ?inE => ->; exists (existT _ _ cptK) => // z Cz; exists O. +move=> _ ->; exists (fset1 C) => //; last by rewrite set_fset1 bigcap_set1. +by move=> _ /[!inE] ->; exists (existT _ _ cptK) => // z Cz; exists O. Qed. End compact_open. @@ -6803,10 +6800,10 @@ End compact_open. Lemma compact_closedI {T : topologicalType} (A B : set T) : compact A -> closed B -> compact (A `&` B). Proof. -move=> cptA clB F PF FAB; have FA : F A by move: FAB; apply: filterS. +move=> cptA clB F PF FAB; have FA : F A by move: FAB; exact: filterS. (have FB : F B by move: FAB; apply: filterS); have [x [Ax]] := cptA F PF FA. move=> /[dup] clx; rewrite {1}clusterE => /(_ (closure B)); move: clB. -by rewrite closure_id => /[dup] + <- => <- /(_ FB) Bx; exists x; split. +by rewrite closure_id => /[dup] + <- => <- /(_ FB) Bx; exists x. Qed. Notation "{ 'compact-open' , U -> V }" := (@compact_open U V). @@ -6819,44 +6816,44 @@ Context {U : topologicalType} {V : uniformType}. Let small_ent_sub := @small_set_sub _ (@entourage V). Lemma compact_open_fam_compactP (f : U -> V) (F : set (set (U -> V))) : - continuous f -> (Filter F) -> + continuous f -> Filter F -> {compact-open, F --> f} <-> {family compact, F --> f}. Proof. move=> ctsf FF; split; first last. move=> cptF; apply/compact_open_cvgP => K O cptK oO fKO. apply: cptF; have := fam_compact_nbhs oO fKO cptK ctsf; apply: filter_app. - by near=> g => /= gKO ? [z Kx <-]; apply: gKO. -move/compact_open_cvgP=> cptOF; apply/cvg_sup; case=> K cptK R. + by near=> g => /= gKO ? [z Kx <-]; exact: gKO. +move/compact_open_cvgP=> cptOF; apply/cvg_sup => -[K cptK R]. case=> D [[E oE <-] Ekf] /filterS; apply. -move: oE; rewrite openE => /(_ _ Ekf); case => ? [J entJ] EKR KfE. -near=> z; apply/KfE/EKR; case => u Kp; rewrite /= /set_val /= /eqincl /incl. +move: oE; rewrite openE => /(_ _ Ekf); case => A [J entJ] EKR KfE. +near=> z; apply/KfE/EKR => -[u Kp]; rewrite /= /set_val /= /eqincl /incl. (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/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 C := f @^-1` to_set E' (f u). pose B := \bigcup_(z in K `&` closure C) interior (to_set E' (f z)). have oB : open B by apply: bigcup_open => ? ?; exact: open_interior. have fKB : f @` (K `&` closure C) `<=` B. - move=> ? [z ? <-]; exists z => //; rewrite /interior. + move=> _ [z KCz <-]; exists z => //; rewrite /interior. by rewrite -nbhs_entourageE; exists E'. have cptKC : compact (K `&` closure C). by apply: compact_closedI => //; exact: closed_closure. have := cptOF (K `&` closure C) B cptKC oB fKB. -exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). +exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). split; last exact: cptOF. by apply: (ctsf) => //; rewrite /filter_of -nbhs_entourageE; exists E'. case=> z h /= [Cz KB Kz]. -case: (KB (h z)); first by (exists z; split => //; apply: subset_closure). -move=> w [Kw Cw /interior_subset Jfwhz]; apply:subset_split_ent => //. -exists (f w); last apply:(near (small_ent_sub _) E') => //. +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') => //. apply: subset_split_ent => //; exists (f u). - apply entourage_sym; apply:(near (small_ent_sub _) E') => //. + by apply/entourage_sym; apply: (near (small_ent_sub _) E'). have [] := Cw (f@^-1` (to_set E' (f w))). by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r). - by apply:(near (small_ent_sub _) E') => //. -by apply entourage_sym; apply:(near (small_ent_sub _) E') => //. + exact: (near (small_ent_sub _) E'). +by apply/entourage_sym; apply: (near (small_ent_sub _) E'). Unshelve. all: by end_near. Qed. End compact_open_uniform. @@ -8263,7 +8260,7 @@ Implicit Types (I : Type). Definition equicontinuous {I} (W : set I) (d : I -> (X -> Y)) := forall x (E : set (Y * Y)), entourage E -> - \forall y \near x, forall i, W i -> E(d i x, d i y). + \forall y \near x, forall i, W i -> E (d i x, d i y). Lemma equicontinuous_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y} : @@ -8427,10 +8424,11 @@ Lemma pointwise_precompact_equicontinuous (W : set (X -> Y)) : Proof. move=> /pointwise_precompact_precompact + ectsW. rewrite ?precompactE compact_ultra compact_ultra pointwise_compact_closure //. -move=> /= + F UF FcW => /(_ F UF); rewrite image_id; case => // p [cWp Fp]. -exists p; split => //; apply/(pointwise_compact_cvg) => //. +move=> /= + F UF FcW => /(_ F UF); rewrite image_id => /(_ FcW)[p [cWp Fp]]. +exists p; split => //; apply/pointwise_compact_cvg => //. apply/near_powerset_filter_fromP; first exact: equicontinuous_subset_id. -exists (closure (W : set {ptws X -> Y })) => //; exact: equicontinuous_closure. +exists (closure (W : set {ptws X -> Y })) => //. +exact: equicontinuous_closure. Qed. Section precompact_equicontinuous. @@ -8494,8 +8492,8 @@ End ArzelaAscoli. Lemma uniform_regular {T : uniformType} : @regular T. Proof. -move=> x R; rewrite /= -{1}nbhs_entourageE; case=> E entE ER. -pose E' := (split_ent E); have ? : entourage E' by exact: entourage_split_ent. +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). rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. exact: filterI. @@ -8516,117 +8514,118 @@ Local Notation "U '~>' V" := Section cartesian_closed. Context {U V W : topologicalType}. -(* In this section, we consider under what conditions - [f in U ~> V ~> W | continuous f /\ forall u, continuous (f u)] - and - [f in U * V ~> W | continuous f] - are homeomorphic - - Always: - curry sends cts functions to cts functions - - V locally_compact + regular or hausdorff - uncurry sends cts functions to cts functions - - U regular or hausdorff - curry itself is a continuous map - - U regular or hausdorff AND V locally_compact + regular or hausdorff - uncurry itself is a continuous map - Therefore curry/uncurry are homeomorphisms - So the category of locally compact regular spaces is cartesian closed +(**md In this section, we consider under what conditions \ + `[f in U ~> V ~> W | continuous f /\ forall u, continuous (f u)]` \ + and \ + `[f in U * V ~> W | continuous f]` \ + are homeomorphic. + - Always: \ + `curry` sends continuous functions to continuous functions. + - `V` locally_compact + regular or Hausdorff: \ + `uncurry` sends continuous functions to continuous functions. + - `U` regular or Hausdorff: \ + `curry` itself is a continuous map. + - `U` regular or Hausdorff AND `V` locally_compact + regular or Hausdorff \ + `uncurry` itself is a continuous map. \ + Therefore `curry`/`uncurry` are homeomorphisms. + + So the category of locally compact regular spaces is cartesian closed. *) Lemma continuous_curry (f : U * V ~> W) : continuous f -> - continuous (curry f : (U ~> V ~> W)) /\ forall u, continuous (curry f u). + continuous (curry f : U ~> V ~> W) /\ forall u, continuous (curry f u). Proof. -move=> ctsf; split; first last. +move=> ctsf; split; first last. move=> u z; apply: continuous_comp; last exact: ctsf. by apply: cvg_pair => //=; exact: cvg_cst. move=> x; apply/compact_open_cvgP => K O /= cptK oO fKO. near=> z => w /= [+ + <-]; near: z. -move/compact_near_coveringP/near_covering_withinP: cptK; apply. -move=> v Kv; have [[P Q] [Px Qv] PQfO]: nbhs (x,v) (f@^-1` O). +move/compact_near_coveringP/near_covering_withinP : cptK; apply. +move=> v Kv; have [[P Q] [Px Qv] PQfO] : nbhs (x, v) (f @^-1` O). by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. -by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; exact: PQfO. +by exists (Q, P) => // -[b a] /= [Qb Pa] Kb; exact: PQfO. Unshelve. all: by end_near. Qed. -Lemma continuous_uncurry_regular (f : U ~> V ~> W): +Lemma continuous_uncurry_regular (f : U ~> V ~> W) : locally_compact [set: V] -> @regular V -> continuous f -> - (forall u, continuous (f u)) -> continuous (uncurry f : ((U * V) ~> W)). + (forall u, continuous (f u)) -> continuous (uncurry f : U * V ~> W). Proof. -move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv] /filterS. -apply; have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. +move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE => -[O [oO Ofuv]] /filterS. +apply; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB]. have [R Rv RO] : exists2 R, nbhs v R & forall z, closure R z -> O (f u z). - have [] := reg v ((f u)@^-1` O); first by apply: cfp; exact: open_nbhs_nbhs. + have [] := reg v (f u @^-1` O); first by apply: cfp; exact: open_nbhs_nbhs. by move=> R ? ?; exists R. -exists (f @^-1` ([set g | g @` (B `&` closure R) `<=` O]), (B `&` closure R)). +exists (f @^-1` [set g | g @` (B `&` closure R) `<=` O], B `&` closure R). split; [apply/cf/open_nbhs_nbhs; split | apply: filterI] => //. - apply: compact_open_open => //; apply: compact_closedI => //. exact: closed_closure. - by move=> ? [x [? + <-]]; apply: RO. - - by apply: filterS; [exact: subset_closure|]. + - by apply: filterS; first exact: subset_closure. by case=> a r /= [fBMO [Br] cmR]; apply: fBMO; exists r. Qed. -Lemma continuous_uncurry (f : U ~> V ~> W): +Lemma continuous_uncurry (f : U ~> V ~> W) : locally_compact [set: V] -> hausdorff_space V -> continuous f -> (forall u, continuous (f u)) -> - continuous ((uncurry : (U ~> V ~> W) -> ((U * V) ~> W)) f). + continuous ((uncurry : (U ~> V ~> W) -> (U * V ~> W)) f). Proof. -move=> lcV hsdf ? ?; apply: continuous_uncurry_regular => //. -move=> v; have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. -by move=> z; apply: (@compact_regular V hsdf v B). +move=> lcV hsdf ctsf cf; apply: continuous_uncurry_regular => //. +move=> v; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB]. +by move=> z; exact: (@compact_regular V hsdf v B). Qed. Lemma curry_continuous (f : U * V ~> W) : continuous f -> @regular U -> - {for f, continuous ((curry : ((U * V) ~> W) -> (U ~> V ~> W)))}. + {for f, continuous (curry : (U * V ~> W) -> (U ~> V ~> W))}. Proof. move=> ctsf regU; apply/compact_open_cvgP. - by apply: fmap_filter; exact:nbhs_filter. + by apply: fmap_filter; exact: nbhs_filter. move=> K ? cptK [D OfinIo <-] fKD /=; near=> z => w [+ + <-]; near: z. move/compact_near_coveringP/near_covering_withinP : (cptK); apply => u Ku. have [] := fKD (curry f u); first by exists u. -move=> E /[dup]/[swap]/OfinIo [N Asub <- DIN INf]. +move=> E /[dup] /[swap] /OfinIo [N Asub <- DIN INf]. suff : \forall x' \near u & i \near nbhs f, K x' -> (\bigcap_(i in [set` N]) i) (curry i x'). apply: filter_app; near=> a b => /[apply] ?. by exists (\bigcap_(i in [set` N]) i). -apply: filter_bigI_within=> R RN; have /set_mem [[M cptM _]] := Asub _ RN. +apply: filter_bigI_within => R RN; have /set_mem [[M cptM _]] := Asub _ RN. have Rfu : R (curry f u) by exact: INf. -case/(_ _ Rfu) => O [fMO oO] MOR; near=> p => /= Ki; apply: MOR => + [+ + <-]. +move/(_ _ Rfu) => [O [fMO oO] MOR]; near=> p => /= Ki; apply: MOR => + [+ + <-]. move=> _ v Mv; move: v Mv Ki; near: p. -have umb : \forall y \near u, (forall b, M b -> nbhs (y, b) (f@^-1` O) ). +have umb : \forall y \near u, (forall b, M b -> nbhs (y, b) (f @^-1` O)). move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. - have [[P Q] [Pu Qv] PQO] : nbhs (u,v) (f@^-1` O). + have [[P Q] [Pu Qv] PQO] : nbhs (u, v) (f @^-1` O). by apply: ctsf; apply: open_nbhs_nbhs; split => //; apply: fMO; exists v. - exists (Q, P); [by split| case => b a [Qb Pa Mb]]. - by apply: ctsf; apply: open_nbhs_nbhs; split => //; apply: PQO. + exists (Q, P); [by []| move=> [b a [/= Qb Pa Mb]]]. + by apply: ctsf; apply: open_nbhs_nbhs; split => //; exact: PQO. move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. have [P' P'u cPO] := regU u _ umb. -pose L := [set h | h @`((K `&` (closure P'))`*`M) `<=` O]. -exists (setT, (P' `*` L)). +pose L := [set h | h @` ((K `&` closure P') `*` M) `<=` O]. +exists (setT, P' `*` L). split => //; [exact: filterT|]; exists (P', L) => //; split => //. apply: open_nbhs_nbhs; split; first apply: compact_open_open => //. apply: compact_setM => //; apply: compact_closedI => //. exact: closed_closure. by move=> ? [[a b] [[Ka /cPO +] Mb <-]] => /(_ _ Mb)/nbhs_singleton. -case => b [a h] [? [Pa] +] Ma Ka; apply. -exists (a,b); split => //; split => //; apply/subset_closure => //. +move=> [b [a h]] [/= _ [Pa] +] Ma Ka; apply. +by exists (a, b); split => //; split => //; exact/subset_closure. Unshelve. all: by end_near. Qed. Lemma uncurry_continuous (f : U ~> V ~> W) : locally_compact [set: V] -> @regular V -> @regular U -> continuous f -> (forall u, continuous (f u)) -> - {for f, continuous ((uncurry : (U ~> V ~> W) -> (U * V ~> W)))}. + {for f, continuous (uncurry : (U ~> V ~> W) -> (U * V ~> W))}. Proof. move=> lcV regV regU ctsf ctsfp; apply/compact_open_cvgP. by apply: fmap_filter; exact:nbhs_filter. move=> /= K O cptK oO fKO; near=> h => ? [+ + <-]; near: h. move/compact_near_coveringP/near_covering_withinP: (cptK); apply. case=> u v Kuv. -have : exists P Q, [/\ closed P, compact Q, nbhs u P, +have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. - have : continuous (uncurry f) by apply: continuous_uncurry_regular. - move/continuousP/(_ _ oO); rewrite openE => /(_ (u,v)) []. - by apply: fKO; exists (u,v). + have : continuous (uncurry f) by exact: continuous_uncurry_regular. + move/continuousP/(_ _ oO); rewrite openE => /(_ (u, v))[]. + by apply: fKO; exists (u, v). case=> /= P' Q' [P'u Q'v] PQO. have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. have [P Pu cPP'] := regU u P' P'u; have [Q Qv cQQ'] := regV v Q' Q'v. @@ -8637,21 +8636,23 @@ have : exists P Q, [/\ closed P, compact Q, nbhs u P, - by apply: filterI=> //; apply: filterS; first exact: subset_closure. - by case => a b [/cPP' ?] [_ /cQQ' ?]; exact: PQO. case=> P [Q [clP cptQ Pu Qv PQfO]]; pose R := [set g : V ~> W | g @` Q `<=` O]. -(have oR : open R by exact: compact_open_open); pose P' := f@^-1` R. +(have oR : open R by exact: compact_open_open); pose P' := f @^-1` R. pose L := [set h : U ~> V ~> W | h @` (fst @` K `&` P) `<=` R]. -exists (((P`&` P') `*` Q), L); first split => /=. +exists ((P `&` P') `*` Q, L); first split => /=. - exists (P `&` P', Q) => //; split => //=; apply: filterI => //. - apply: ctsf; apply: open_nbhs_nbhs; split => // ? [b ? <-]. - by apply: (PQfO (u,b)); split => //; exact: nbhs_singleton. + apply: ctsf; apply: open_nbhs_nbhs; split => // _ [b Qb <-]. + by apply: (PQfO (u, b)); split => //; exact: nbhs_singleton. - rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. apply: compact_open_open => //; apply: compact_closedI => //. - apply: continuous_compact => //; apply: continuous_subspaceT => ?. + apply: continuous_compact => //; apply: continuous_subspaceT => x. exact: cvg_fst. - move=> /= ? [a [Pa ?] <-] ? [b Qb <-]. - by apply: (PQfO (a,b)); split => //; apply: nbhs_singleton. -case; case => a b h [/= [[? ?] ? Lh] ?]. -apply: (Lh (h a)); first by exists a => //; split => //; exists (a,b). + move=> /= _ [a [Kxa Pa] <-] _ [b Qb <-]. + by apply: (PQfO (a, b)); split => //; exact: nbhs_singleton. +move=> [[a b h]] [/= [[Pa P'a] Qb Lh] Kab]. +apply: (Lh (h a)); first by exists a => //; split => //; exists (a, b). by exists b. Unshelve. all: by end_near. Qed. + End cartesian_closed. -End currying. \ No newline at end of file + +End currying. From bfdfa9575f36b4d39a4e542843086bb082ff00b9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jan 2024 16:03:46 +0900 Subject: [PATCH 14/15] doc --- theories/topology.v | 55 ++++++++++++++++++++++++--------------------- 1 file changed, 30 insertions(+), 25 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index d05a8c7165..690fb68a98 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -299,8 +299,10 @@ Require Import reals signed. (* for a finite number of indices in D *) (* cover_compact == set of compact sets w.r.t. the open *) (* cover-based definition of compactness *) +(* regular == regular space *) (* near_covering == a reformulation of covering compact *) (* better suited for use with `near` *) +(* near_covering_within == equivalent definition of near_covering *) (* kolmogorov_space T <-> T is a Kolmogorov space (T0) *) (* accessible_space T <-> T is an accessible space (T1) *) (* close x y <-> x and y are arbitrarily close w.r.t. *) @@ -449,26 +451,29 @@ Require Import reals signed. (* *) (* ### Function space topologies *) (* ``` *) -(* {uniform` A -> V} == the space U -> V, equipped with the topology of *) -(* uniform convergence from a set A to V, where *) -(* V is a uniformType *) -(* {uniform U -> V} := {uniform` [set: U] -> V} *) -(* {uniform A, F --> f} == F converges to f in {uniform A -> V} *) -(* {uniform, F --> f} := {uniform setT, F --> f} *) -(* {ptws U -> V} == the space U -> V, equipped with the topology of *) -(* pointwise convergence from U to V, where V is a *) -(* topologicalType *) -(* This is a notation for @fct_Pointwise U V. *) -(* {ptws, F --> f} == F converges to f in {ptws U -> V} *) -(* {family fam, U -> V} == The space U -> V, equipped with the supremum *) -(* topology of {uniform A -> f} for each A in 'fam' *) -(* In particular {family compact, U -> V} is the *) -(* topology of compact convergence. *) -(* {family fam, F --> f} == F converges to f in {family fam, U -> V} *) +(* {uniform` A -> V} == the space U -> V, equipped with the topology *) +(* of uniform convergence from a set A to V, where *) +(* V is a uniformType *) +(* {uniform U -> V} := {uniform` [set: U] -> V} *) +(* {uniform A, F --> f} == F converges to f in {uniform A -> V} *) +(* {uniform, F --> f} := {uniform setT, F --> f} *) +(* {ptws U -> V} == the space U -> V, equipped with the topology of *) +(* pointwise convergence from U to V, where V is *) +(* a topologicalType *) +(* This is a notation for @fct_Pointwise U V. *) +(* {ptws, F --> f} == F converges to f in {ptws U -> V} *) +(* {family fam, U -> V} == the space U -> V, equipped with the supremum *) +(* topology of {uniform A -> f} for each A in *) +(* 'fam' *) +(* In particular {family compact, U -> V} is the *) +(* topology of compact convergence. *) +(* {family fam, F --> f} == F converges to f in {family fam, U -> V} *) +(* {compact_open, U -> V} == compact-open topology *) +(* {compact_open, F --> f} == F converges to f in {compact_open, U -> V} *) (* *) -(* dense S == the set (S : set T) is dense in T, with T of *) -(* type topologicalType *) -(* weak_pseudoMetricType == the metric space for weak topologies *) +(* dense S == the set (S : set T) is dense in T, with T of *) +(* type topologicalType *) +(* weak_pseudoMetricType == the metric space for weak topologies *) (* ``` *) (* *) (* ### Subspaces of topological spaces *) @@ -6617,7 +6622,7 @@ Qed. Definition fct_UniformFamily (fam : (set U) -> Prop) := U -> V. -Definition family_cvg_uniformType (fam: set U -> Prop) := +Definition family_cvg_uniformType (fam : set U -> Prop) := @sup_uniformType _ (sigT fam) (fun k => Uniform.class (@fct_restrictedUniformType U (projT1 k) V)). @@ -6712,15 +6717,15 @@ case=> y g [/= Efxy] AEg Ay; apply: EfO; apply: subset_split_ent => //. by exists (f y) => //=; exact: AEg. Unshelve. all: by end_near. Qed. -(* It turns out {family compact, U -> V} can be generalized to only assume *) -(* `topologicalType` on V. This topology is called the compact-open topology. *) -(* This topology is special because it is the _only_ topology that will allow *) -(* curry/uncurry to be continuous. *) +(**md It turns out `{family compact, U -> V}` can be generalized to only assume + `topologicalType` on `V`. This topology is called the compact-open topology. + This topology is special because it is the _only_ topology that will allow + `curry`/`uncurry` to be continuous. *) Section compact_open. Context {T U : topologicalType}. -Definition compact_open : Type := T->U. +Definition compact_open : Type := T -> U. Section compact_open_setwise. Context {K : set T}. From 95dceaf726486e83b888e996c8e285b89ce066ae Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 17 Jan 2024 22:57:47 -0500 Subject: [PATCH 15/15] removing regular in favor of regular_space --- CHANGELOG_UNRELEASED.md | 1 - theories/topology.v | 96 ++++++++++++++++++++--------------------- 2 files changed, 46 insertions(+), 51 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0999ff4e41..b08b5c18b9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,7 +22,6 @@ + definition `near_covering_within` + lemma `near_covering_withinP` + lemma `compact_setM` - + definition `regular` + lemma `compact_regular` + lemma `fam_compact_nbhs` + definition `compact_open`, notation `{compact-open, U -> V}` diff --git a/theories/topology.v b/theories/topology.v index 690fb68a98..4e95029c6b 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -299,7 +299,6 @@ Require Import reals signed. (* for a finite number of indices in D *) (* cover_compact == set of compact sets w.r.t. the open *) (* cover-based definition of compactness *) -(* regular == regular space *) (* near_covering == a reformulation of covering compact *) (* better suited for use with `near` *) (* near_covering_within == equivalent definition of near_covering *) @@ -3651,8 +3650,40 @@ move=> /DsubC /= [y /= yfs hyz]; exists (h' y) => //. by rewrite set_imfset /=; exists y. Qed. -Definition regular {T : topologicalType} := forall x : T, - filter_from (nbhs x) closure --> x. +Section set_nbhs. +Context {T : topologicalType} (A : set T). + +Definition set_nbhs := \bigcap_(x in A) nbhs x. + +Global Instance set_nbhs_filter : Filter set_nbhs. +Proof. +split => P Q; first by exact: filterT. + by move=> Px Qx x Ax; apply: filterI; [exact: Px | exact: Qx]. +by move=> PQ + x Ax => /(_ _ Ax)/filterS; exact. +Qed. + +Global Instance set_nbhs_pfilter : A!=set0 -> ProperFilter set_nbhs. +Proof. +case=> x Ax; split; last exact: set_nbhs_filter. +by move/(_ x Ax)/nbhs_singleton. +Qed. + +Lemma set_nbhsP (B : set T) : + set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]). +Proof. +split; first last. + by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs. +move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B]. + have [/snB|?] := pselect (A x); last by exists point. + by rewrite nbhsE => -[V [? ? ?]]; exists V. +exists (\bigcup_(x in A) (projT1 (cid (Ux x)))); split. +- by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)). +- by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)). +- by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact. +Qed. + +End set_nbhs. + Section separated_topologicalType. Variable T : topologicalType. @@ -3769,6 +3800,13 @@ rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. by rewrite inE; apply: VUc; rewrite -inE. Qed. +Definition normal_space := + forall A : set T, closed A -> + filter_from (set_nbhs A) closure `=>` set_nbhs A. + +Definition regular_space := + forall a : T, filter_from (nbhs a) closure --> a. + Hypothesis sep : hausdorff_space T. Lemma closeE x y : close x y = (x = y). @@ -3813,7 +3851,7 @@ Proof. move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl. Qed. -Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular}. +Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular_space}. Proof. move=> cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //. - apply: filter_from_proper => //; first last. @@ -4238,40 +4276,6 @@ Qed. End totally_disconnected. -Section set_nbhs. -Context {T : topologicalType} (A : set T). - -Definition set_nbhs := \bigcap_(x in A) nbhs x. - -Global Instance set_nbhs_filter : Filter set_nbhs. -Proof. -split => P Q; first by exact: filterT. - by move=> Px Qx x Ax; apply: filterI; [exact: Px | exact: Qx]. -by move=> PQ + x Ax => /(_ _ Ax)/filterS; exact. -Qed. - -Global Instance set_nbhs_pfilter : A!=set0 -> ProperFilter set_nbhs. -Proof. -case=> x Ax; split; last exact: set_nbhs_filter. -by move/(_ x Ax)/nbhs_singleton. -Qed. - -Lemma set_nbhsP (B : set T) : - set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]). -Proof. -split; first last. - by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs. -move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B]. - have [/snB|?] := pselect (A x); last by exists point. - by rewrite nbhsE => -[V [? ? ?]]; exists V. -exists (\bigcup_(x in A) (projT1 (cid (Ux x)))); split. -- by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)). -- by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)). -- by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact. -Qed. - -End set_nbhs. - (** Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -8246,14 +8250,6 @@ exact: iter_split_ent. Qed. End gauges. - -Definition normal_space (T : topologicalType) := - forall A : set T, closed A -> - set_nbhs A `<=` filter_from (set_nbhs A) closure. - -Definition regular_space (T : topologicalType) := - forall a : T, nbhs a `<=` filter_from (nbhs a) closure. - Section ArzelaAscoli. Context {X : topologicalType}. Context {Y : uniformType}. @@ -8495,7 +8491,7 @@ Qed. End ArzelaAscoli. -Lemma uniform_regular {T : uniformType} : @regular T. +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. @@ -8553,7 +8549,7 @@ by exists (Q, P) => // -[b a] /= [Qb Pa] Kb; exact: PQfO. Unshelve. all: by end_near. Qed. Lemma continuous_uncurry_regular (f : U ~> V ~> W) : - locally_compact [set: V] -> @regular V -> continuous f -> + locally_compact [set: V] -> @regular_space V -> continuous f -> (forall u, continuous (f u)) -> continuous (uncurry f : U * V ~> W). Proof. move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE => -[O [oO Ofuv]] /filterS. @@ -8580,7 +8576,7 @@ move=> v; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB]. by move=> z; exact: (@compact_regular V hsdf v B). Qed. -Lemma curry_continuous (f : U * V ~> W) : continuous f -> @regular U -> +Lemma curry_continuous (f : U * V ~> W) : continuous f -> @regular_space U -> {for f, continuous (curry : (U * V ~> W) -> (U ~> V ~> W))}. Proof. move=> ctsf regU; apply/compact_open_cvgP. @@ -8617,7 +8613,7 @@ by exists (a, b); split => //; split => //; exact/subset_closure. Unshelve. all: by end_near. Qed. Lemma uncurry_continuous (f : U ~> V ~> W) : - locally_compact [set: V] -> @regular V -> @regular U -> + locally_compact [set: V] -> @regular_space V -> @regular_space U -> continuous f -> (forall u, continuous (f u)) -> {for f, continuous (uncurry : (U ~> V ~> W) -> (U * V ~> W))}. Proof.