diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 30570d33e4..60b4b08995 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -69,6 +69,17 @@ + new lemmas `pi_continuous`, `quotient_continuous`, and `repr_comp_continuous`. +- in file `boolp.v`, + + new lemma `forallp_asboolPn2`. +- in file `classical_sets.v`, + + new lemma `preimage_range`. +- in file `topology.v`, + + new definitions `hausdorff_accessible`, `separate_points_from_closed`, and + `join_product`. + + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, + `join_product_continuous`, `join_product_open`, `join_product_inj`, and + `join_product_weak`. + ### Changed - in `fsbigop.v`: diff --git a/classical/boolp.v b/classical/boolp.v index 7ff24a1c8a..7d2d0ba576 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -676,6 +676,14 @@ split=> [[x Px NQx] /(_ x Px)//|]; apply: contra_notP => + x Px. by apply: contra_notP => NQx; exists x. Qed. +Lemma forallp_asboolPn2 {T} {P Q : T -> Prop} : + reflect (forall x : T, ~ P x \/ ~ Q x) (~~ `[]). +Proof. +apply: (iffP idP)=> [/asboolPn NP x|NP]. + by move/forallPNP : NP => /(_ x)/and_rec/not_andP. +by apply/asboolP=> -[x Px Qx]; have /not_andP := NP x; exact. +Qed. + Module FunOrder. Section FunOrder. Import Order.TTheory. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index e647c855cb..42f7c9f835 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1279,6 +1279,9 @@ Proof. by case=> [t ?]; exists (f t). Qed. Lemma preimage_image f A : A `<=` f @^-1` (f @` A). Proof. by move=> a Aa; exists a. Qed. +Lemma preimage_range {A B : Type} (f : A -> B) : f @^-1` (range f) = [set: A]. +Proof. by rewrite eqEsubset; split=> x // _; exists x. Qed. + Lemma image_preimage_subset f Y : f @` (f @^-1` Y) `<=` Y. Proof. by move=> _ [t /= Yft <-]. Qed. diff --git a/theories/normedtype.v b/theories/normedtype.v index d2e2159cb6..d2f2474160 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -3940,26 +3940,26 @@ Qed. Lemma nbhs_open_ereal_lt r (f : R -> R) : r < f r -> nbhs r%:E [set y | y < (f r)%:E]%E. Proof. -move=> xfx; rewrite nbhsE /=; eexists; split; last by move=> y; exact. +move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact. by split; [apply open_ereal_lt_ereal | rewrite /= lte_fin]. Qed. Lemma nbhs_open_ereal_gt r (f : R -> R) : f r < r -> nbhs r%:E [set y | (f r)%:E < y]%E. Proof. -move=> xfx; rewrite nbhsE /=; eexists; split; last by move=> y; exact. +move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact. by split; [apply open_ereal_gt_ereal | rewrite /= lte_fin]. Qed. Lemma nbhs_open_ereal_pinfty r : (nbhs +oo [set y | r%:E < y])%E. Proof. -rewrite nbhsE /=; eexists; split; last by move=> y; exact. +rewrite nbhsE /=; eexists; last by move=> y; exact. by split; [apply open_ereal_gt_ereal | rewrite /= ltry]. Qed. Lemma nbhs_open_ereal_ninfty r : (nbhs -oo [set y | y < r%:E])%E. Proof. -rewrite nbhsE /=; eexists; split; last by move=> y; exact. +rewrite nbhsE /=; eexists; last by move=> y; exact. by split; [apply open_ereal_lt_ereal | rewrite /= ltNyr]. Qed. @@ -4290,7 +4290,7 @@ move=> oU; have [->|U0] := eqVneq U set0. apply/seteqP; split=> [x Ux|x [p _ Ipx]]; last exact: bigcup_ointsub_sub Ipx. suff [q Iqx] : exists q, bigcup_ointsub U q x. by exists q => //=; rewrite in_setE; case: Iqx => A [[_ _ +] ? _]; exact. -have : nbhs x U by rewrite nbhsE /=; exists U; split => //. +have : nbhs x U by rewrite nbhsE /=; exists U. rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ => -[_/posnumP[r] xrU]. have /rat_in_itvoo[q qxxr] : (x - r%:num < x + r%:num)%R. by rewrite ltr_subl_addr -addrA ltr_addl. @@ -4804,7 +4804,7 @@ move=> C D FC f_D; have {}f_D : have exPj : forall j, exists Bj, open_nbhs (f j) Bj /\ Bj `<=` E ord0 j. move=> j; have := f_E ord0 j; rewrite nbhsE => - [Bj]. by rewrite row_simpl'; exists Bj. - exists [set g | forall j, (get (Pj j)) (g j)]; split; last first. + exists [set g | forall j, (get (Pj j)) (g j)]; last first. move=> g Pg; apply: sED => i j; rewrite ord1 row_simpl'. by have /getPex [_ /(_ _ (Pg j))] := exPj j. split; last by move=> j; have /getPex [[]] := exPj j. diff --git a/theories/sequences.v b/theories/sequences.v index 568fbf6ad9..5ddf525490 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1282,8 +1282,7 @@ Lemma cvg_nseries_near (u : nat^nat) : cvg (nseries u) -> \forall n \near \oo, u n = 0%N. Proof. move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l]. - exists [set l]; split; last by split. - by exists [set l] => //; rewrite bigcup_set1. + by exists [set l]; split=> //; exists [set l] => //; rewrite bigcup_set1. have /ul[b _ bul] : nbhs l [set l.-1; l]. by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1. exists (maxn a b) => // n /= abn. diff --git a/theories/topology.v b/theories/topology.v index dfba897265..b8ba388b9a 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -116,6 +116,13 @@ Require Import reals signed. (* \oo == "eventually" filter on nat: set of *) (* predicates on natural numbers that are *) (* eventually true. *) +(* separate_points_from_closed f == For a closed set U and point x outside *) +(* some member of the family f sends *) +(* f_i(x) outside (closure (f_i @` U)). *) +(* Used together with join_product. *) +(* join_product f == The function (x => f ^~ x). When the *) +(* family f separates points from closed *) +(* sets, join_product is an embedding. *) (* *) (* * Near notations and tactics: *) (* --> The purpose of the near notations and tactics is to make the *) @@ -1592,7 +1599,7 @@ Record mixin_of (T : Type) (nbhs : T -> set (set T)) := Mixin { open : set (set T) ; ax1 : forall p : T, ProperFilter (nbhs p) ; ax2 : forall p : T, nbhs p = - [set A : set T | exists B : set T, open B /\ B p /\ B `<=` A] ; + [set A : set T | exists B : set T, [/\ open B, B p & B `<=` A] ] ; ax3 : open = [set A : set T | A `<=` nbhs^~ A ] }. @@ -1671,17 +1678,17 @@ Proof. exact: (@nbhs_pfilter). Qed. Canonical nbhs_filter_on (x : T) := FilterType (nbhs x) (@nbhs_filter x). Lemma nbhsE (p : T) : - nbhs p = [set A : set T | exists B : set T, open_nbhs p B /\ B `<=` A]. + nbhs p = [set A : set T | exists2 B : set T, open_nbhs p B & B `<=` A]. Proof. -have -> : nbhs p = [set A : set T | exists B, open B /\ B p /\ B `<=` A]. +have -> : nbhs p = [set A : set T | exists B, [/\ open B, B p & B `<=` A] ]. exact: Topological.ax2. -by rewrite predeqE => A; split=> [[B [? []]]|[B [[]]]]; exists B. +by rewrite predeqE => A; split=> [[B [?]]|[B[]]]; exists B. Qed. Lemma open_nbhsE (p : T) (A : set T) : open_nbhs p A = (open A /\ nbhs p A). Proof. -rewrite nbhsE propeqE; split=> [[? ?]|[? [B [[? ?] BA]]]]; split => //; - [by exists A; split | exact: BA]. +by rewrite nbhsE propeqE; split=> [[? ?]|[? [B [? ?] BA]]]; split => //; + [exists A | exact: BA]. Qed. Definition interior (A : set T) := (@nbhs _ T)^~ A. @@ -1690,19 +1697,19 @@ Local Notation "A ^°" := (interior A). Lemma interior_subset (A : set T) : A^° `<=` A. Proof. -by move=> p; rewrite /interior nbhsE => -[? [[??]]]; apply. +by move=> p; rewrite /interior nbhsE => -[? [? ?]]; apply. Qed. Lemma openE : open = [set A : set T | A `<=` A^°]. Proof. exact: Topological.ax3. Qed. Lemma nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p. -Proof. by rewrite nbhsE => - [? [[_ ?]]]; apply. Qed. +Proof. by rewrite nbhsE => - [? [_ ?]]; apply. Qed. Lemma nbhs_interior (p : T) (A : set T) : nbhs p A -> nbhs p A^°. Proof. -rewrite nbhsE /open_nbhs openE => - [B [[Bop Bp] sBA]]. -by exists B; split=> // q Bq; apply: filterS sBA _; apply: Bop. +rewrite nbhsE /open_nbhs openE => - [B [Bop Bp] sBA]. +by exists B => // q Bq; apply: filterS sBA _; apply: Bop. Qed. Lemma open0 : open set0. @@ -1738,15 +1745,15 @@ Qed. Lemma open_interior (A : set T) : open A^°. Proof. -rewrite openE => p; rewrite /interior nbhsE => - [B [[Bop Bp]]]. +rewrite openE => p; rewrite /interior nbhsE => - [B [Bop Bp]]. by rewrite open_subsetE //; exists B. Qed. Lemma interior_bigcup I (D : set I) (f : I -> set T) : \bigcup_(i in D) (f i)^° `<=` (\bigcup_(i in D) f i)^°. Proof. -move=> p [i Di]; rewrite /interior nbhsE => - [B [[Bop Bp] sBfi]]. -by exists B; split=> // ? /sBfi; exists i. +move=> p [i Di]; rewrite /interior nbhsE => - [B [Bop Bp] sBfi]. +by exists B => // ? /sBfi; exists i. Qed. Lemma open_nbhsT (p : T) : open_nbhs p setT. @@ -1757,14 +1764,14 @@ Lemma open_nbhsI (p : T) (A B : set T) : Proof. by move=> [Aop Ap] [Bop Bp]; split; [apply: openI|split]. Qed. Lemma open_nbhs_nbhs (p : T) (A : set T) : open_nbhs p A -> nbhs p A. -Proof. by rewrite nbhsE => p_A; exists A; split. Qed. +Proof. by rewrite nbhsE => p_A; exists A. Qed. Lemma interiorI (A B:set T): (A `&` B)^° = A^° `&` B^°. Proof. -rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 [?]] | []]. +rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 ?] | []]. - by rewrite subsetI => // -[? ?]; split; exists B0. -- move=> -[B0 [? ?]] [B1 [? ?]]; exists (B0 `&` B1); split; - [exact: open_nbhsI | by rewrite subsetI; split; apply: subIset; [left|right]]. +- by move=> -[B0 ? ?] [B1 ? ?]; exists (B0 `&` B1); + [exact: open_nbhsI | rewrite subsetI; split; apply: subIset; [left|right]]. Qed. End Topological1. @@ -1788,8 +1795,8 @@ Lemma continuousP (S T : topologicalType) (f : S -> T) : continuous f <-> forall A, open A -> open (f @^-1` A). Proof. split=> fcont; first by rewrite !openE => A Aop ? /Aop /fcont. -move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [[Bop Bfs] sBA]]. -by exists (f @^-1` B); split; [split=> //; apply/fcont|move=> ? /sBA]. +move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA]. +by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA]. Qed. Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x : @@ -1915,10 +1922,9 @@ Local Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)). Lemma within_interior (x : T) : A^° x -> within A (nbhs x) = nbhs x. Proof. move=> Aox; rewrite eqEsubset; split; last exact: cvg_within. -rewrite ?nbhsE => W /= => [[B [+ BsubW]]]. +rewrite ?nbhsE => W /= => [[B + BsubW]]. rewrite open_nbhsE => [[oB nbhsB]]. -exists (B `&` A^°); split; last first. - by move=> t /= [] /BsubW + /interior_subset; apply. +exists (B `&` A^°); last by move=> t /= [] /BsubW + /interior_subset; apply. rewrite open_nbhsE; split; first by apply: openI => //; exact: open_interior. by apply: filterI => //; move:(open_interior A); rewrite openE; exact. Qed. @@ -1965,9 +1971,9 @@ Program Definition topologyOfFilterMixin : Topological.mixin_of nbhs' := @Topological.Mixin T nbhs' open_of_nbhs _ _ _. Next Obligation. move=> p; rewrite predeqE => A; split=> [p_A|]; last first. - by move=> [B [Bop [Bp sBA]]]; apply: filterS sBA _; apply: Bop. -exists (nbhs'^~ A); split; first by move=> ?; apply: nbhs'_nbhs'. -by split => // q /nbhs'_singleton. + by move=> [B [Bop Bp sBA]]; apply: filterS sBA _; apply: Bop. +exists (nbhs'^~ A) ; split => //; first by move=> ?; apply: nbhs'_nbhs'. +by move=> q /nbhs'_singleton. Qed. Next Obligation. done. Qed. @@ -1984,19 +1990,19 @@ Hypothesis (op_bigU : forall (I : Type) (f : I -> set T), (forall i, op (f i)) -> op (\bigcup_i f i)). Definition nbhs_of_open (p : T) (A : set T) := - exists B, op B /\ B p /\ B `<=` A. + exists B, [/\ op B, B p & B `<=` A]. Program Definition topologyOfOpenMixin : Topological.mixin_of nbhs_of_open := @Topological.Mixin T nbhs_of_open op _ _ _. Next Obligation. move=> p; apply: Build_ProperFilter. - by move=> A [B [_ [Bp sBA]]]; exists p; apply: sBA. + by move=> A [B [_ Bp sBA]]; exists p; apply: sBA. split; first by exists setT. - move=> A B [C [Cop [Cp sCA]]] [D [Dop [Dp sDB]]]. - exists (C `&` D); split; first exact: opI. - by split=> // q [/sCA Aq /sDB Bq]. -move=> A B sAB [C [Cop [p_C sCA]]]. -by exists C; split=> //; split=> //; apply: subset_trans sAB. + move=> A B [C [Cop Cp sCA]] [D [Dop Dp sDB]]. + exists (C `&` D); split => //; first exact: opI. + by move=> q [/sCA Aq /sDB Bq]. +move=> A B sAB [C [Cop p_C sCA]]. +by exists C; split=> //; apply: subset_trans sAB. Qed. Next Obligation. done. Qed. Next Obligation. @@ -2005,7 +2011,7 @@ rewrite predeqE => A; split=> [Aop p Ap|Aop]. suff -> : A = \bigcup_(B : {B : set T & op B /\ B `<=` A}) projT1 B. by apply: op_bigU => B; have [] := projT2 B. rewrite predeqE => p; split=> [|[B _ Bp]]; last by have [_] := projT2 B; apply. -by move=> /Aop [B [Bop [Bp sBA]]]; exists (existT _ B (conj Bop sBA)). +by move=> /Aop [B [Bop Bp sBA]]; exists (existT _ B (conj Bop sBA)). Qed. End TopologyOfOpen. @@ -2348,12 +2354,12 @@ Lemma cvg_image (F : set (set S)) (s : S) : F --> (s : weak_topologicalType) <-> [set f @` A | A in F] --> f s. Proof. move=> FF fsurj; split=> [cvFs|cvfFfs]. - move=> A /weak_continuous [B [Bop [Bs sBAf]]]. + move=> A /weak_continuous [B [Bop Bs sBAf]]. have /cvFs FB : nbhs (s : weak_topologicalType) B by apply: open_nbhs_nbhs. rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB. exact: image_preimage. -move=> A /= [_ [[B Bop <-] [Bfs sBfA]]]. -have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B; split. +move=> A /= [_ [[B Bop <-] Bfs sBfA]]. +have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B. rewrite nbhs_filterE; apply: filterS FC. by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. @@ -2380,16 +2386,16 @@ Lemma cvg_sup (F : set (set T)) (t : T) : Filter F -> F --> (t : sup_topologicalType) <-> forall i, F --> (t : TS i). Proof. move=> Ffilt; split=> cvFt. - move=> i A /=; rewrite (@nbhsE (TS i)) => - [B [[Bop Bt] sBA]]. + move=> i A /=; rewrite (@nbhsE (TS i)) => - [B [Bop Bt] sBA]. apply: cvFt; exists B; split=> //; exists [set B]; last first. by rewrite predeqE => ?; split=> [[_ ->]|] //; exists B. move=> _ ->; exists [fset B]%fset. by move=> ?; rewrite inE inE => /eqP->; exists i. by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite /= inE // =>/eqP->. move=> A /=; rewrite (@nbhsE sup_topologicalType). -move=> [_ [[[B sB <-] [C BC Ct]] sUBA]]. +move=> [_ [[B sB <-] [C BC Ct] sUBA]]. rewrite nbhs_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C). - by move=> ??; exists C. + by move=> ? ?; exists C. have /sB [D sD IDeC] := BC; rewrite -IDeC; apply: filter_bigI => E DE. have /sD := DE; rewrite inE => - [i _]; rewrite openE => Eop. by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE). @@ -2419,10 +2425,10 @@ Lemma dnbhsE (T : topologicalType) (x : T) : nbhs x = x^' `&` at_point x. Proof. rewrite predeqE => A; split=> [x_A|[x_A Ax]]. split; last exact: nbhs_singleton. - move: x_A; rewrite nbhsE => -[B [x_B sBA]]; rewrite /dnbhs nbhsE. - by exists B; split=> // ? /sBA. -move: x_A; rewrite /dnbhs !nbhsE => -[B [x_B sBA]]; exists B. -by split=> // y /sBA Ay; case: (eqVneq y x) => [->|]. + move: x_A; rewrite nbhsE => -[B [oB x_B sBA]]; rewrite /dnbhs nbhsE. + by exists B => // ? /sBA. +move: x_A; rewrite /dnbhs !nbhsE => -[B [oB x_B sBA]]; exists B => //. +by move=> y /sBA Ay; case: (eqVneq y x) => [->|]. Qed. Global Instance dnbhs_filter {T : topologicalType} (x : T) : Filter x^'. @@ -2453,7 +2459,7 @@ Lemma meets_openr {T : topologicalType} (F : set (set T)) (x : T) : F `#` nbhs x = F `#` open_nbhs x. Proof. rewrite propeqE; split; [exact/meetsSr/open_nbhs_nbhs|]. -by move=> P A B {}/P P; rewrite nbhsE => -[B' [/P + sB]]; apply: subsetI_neq0. +by move=> P A B {}/P P; rewrite nbhsE => -[B' /P + sB]; apply: subsetI_neq0. Qed. Lemma meets_openl {T : topologicalType} (F : set (set T)) (x : T) : @@ -2564,11 +2570,11 @@ Proof. rewrite predeqE => A; split=> Acl p; last first. by move=> clAp; apply: Acl; rewrite -nbhs_nearE => /clAp [? []]. rewrite -nbhs_nearE nbhsE => /asboolP. -rewrite asbool_neg => /forallp_asboolPn clAp. -apply: Acl => B; rewrite nbhsE => - [C [p_C sCB]]. +rewrite asbool_neg => /forallp_asboolPn2 clAp. +apply: Acl => B; rewrite nbhsE => - [C [oC pC]]. have /asboolP := clAp C. -rewrite asbool_neg asbool_and => /nandP [/asboolP//|/existsp_asboolPn [q]]. -move/asboolP; rewrite asbool_neg => /imply_asboolPn [/sCB Bq /contrapT Aq]. +rewrite asbool_or 2!asbool_neg => /orP[/asboolP/not_andP[]//|/existsp_asboolPn [q]]. +move/asboolP; rewrite asbool_neg => /imply_asboolPn[+ /contrapT Aq sCB] => /sCB. by exists q. Qed. @@ -2597,7 +2603,7 @@ Proof. rewrite !closedE=> f_continuous D_cl x /= xDf. apply: D_cl; apply: contra_not xDf => fxD. have NDfx : ~ D (f x). - by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [[??]]]; apply. + by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; apply. by apply: f_continuous fxD; rewrite inE. Qed. @@ -3054,7 +3060,7 @@ Qed. Lemma dfwith_continuous g (i : I) : continuous (dfwith g _ : K i -> PK). Proof. -move=> z U [] P [] [] Q QfinP <- [] [] V JV Vpz. +move=> z U [] P [] [] Q QfinP <- [] V JV Vpz. move/(@preimage_subset _ _ (dfwith g i))/filterS; apply. apply: (@filterS _ _ _ ((dfwith g i) @^-1` V)); first by exists V. have [L Lsub /[dup] VL <-] := QfinP _ JV; rewrite preimage_bigcap. @@ -3242,14 +3248,14 @@ Lemma accessible_closed_set1 : accessible_space -> forall x, closed [set x]. Proof. move=> T1 x; rewrite -[X in closed X]setCK; apply: open_closedC. rewrite openE => y /eqP /T1 [U [oU [yU xU]]]. -rewrite /interior nbhsE /=; exists U; split; last by rewrite subsetC1. -by split=> //; rewrite inE in yU. +rewrite /interior nbhsE /=; exists U; last by rewrite subsetC1. +by split=> //; exact: set_mem. Qed. Lemma accessible_kolmogorov : accessible_space -> kolmogorov_space. Proof. move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split=> //. -by rewrite nbhsE inE; exists A; do !split=> //; rewrite inE in xA. +by rewrite nbhsE inE; exists A => //; rewrite inE in xA. Qed. Lemma accessible_finite_set_closed : @@ -3326,7 +3332,7 @@ rewrite propeqE; split => [T_filterT2|T_openT2] x y. rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB]. move=> /asboolPn; rewrite -set0P => /negP; rewrite negbK => /eqP AIB_eq0. move: xA yB; rewrite !nbhsE. - move=> - [oA [[oA_open oAx] oAA]] [oB [[oB_open oBx] oBB]]. + move=> - [oA [oA_open oAx] oAA] [oB [oB_open oBx] oBB]. by exists (oA, oB); rewrite ?inE; split => //; apply: subsetI_eq0 AIB_eq0. apply: contraPP => /eqP /T_openT2[[/=A B]]. rewrite !inE => - [xA yB] [Aopen Bopen /eqP AIB_eq0]. @@ -3334,6 +3340,13 @@ move=> /(_ A B (open_nbhs_nbhs _) (open_nbhs_nbhs _)). by rewrite -set0P => /(_ _ _)/negP; apply. Qed. +Definition hausdorff_accessible : hausdorff_space T -> accessible_space. +Proof. +rewrite open_hausdorff => hsdfT => x y /hsdfT [[U V] [xU yV]] [/= ? ? /eqP]. +rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. +by rewrite inE; apply: VUc; rewrite -inE. +Qed. + Hypothesis sep : hausdorff_space T. Lemma closeE x y : close x y = (x = y). @@ -3629,7 +3642,7 @@ split. case=> _; rewrite eqEsubset; case=> _ + x Ox => /(_ x I [set x]). by case; [by apply: open_nbhs_nbhs; split |] => y [+ _] => /[swap] -> /eqP. move=> NOx; split; [exact: closedT |]; rewrite eqEsubset; split => x // _. -move=> U; rewrite nbhsE; case=> V [][] oV Vx VU. +move=> U; rewrite nbhsE; case=> V [] oV Vx VU. have Vnx: V != [set x] by apply/eqP => M; apply: (NOx x); rewrite -M. have /existsNP [y /existsNP [Vy Ynx]] : ~ forall y, V y -> y = x. move/negP: Vnx; apply: contra_not => Vxy; apply/eqP; rewrite eqEsubset. @@ -3650,13 +3663,14 @@ Lemma perfect_diagonal (K : nat_topologicalType -> topologicalType) : (forall i, exists (xy: K i * K i), xy.1 != xy.2) -> perfect_set [set: product_topologicalType K]. Proof. -move=> npts; split; [exact: closedT|]; rewrite eqEsubset; split => f // _. +move=> npts; split; first exact: closedT. +rewrite eqEsubset; split => f // _. pose distincts (i : nat) := projT1 (sigW (npts i)). pose derange (i : nat) (z : K i) := if z == (distincts i).1 then (distincts i).2 else (distincts i).1. pose g (N i : nat) := if (i < N)%nat then f i else derange _ (f i). have gcvg : g @ \oo --> (f : product_topologicalType K). - apply/(@cvg_sup (product_topologicalType K)) => N U [V] [[W] oW <-] [] WfN WU. + apply/(@cvg_sup (product_topologicalType K)) => N U [V] [][W] oW <- WfN WU. by apply: (filterS WU); rewrite nbhs_simpl /g; exists N.+1 => // i /= ->. move=> A /gcvg; rewrite nbhs_simpl; case=> N _ An. exists (g N); split => //; last by apply: An; rewrite /= ?leqnn //. @@ -4243,12 +4257,12 @@ Qed. Lemma weak_ent_nbhs : nbhs = nbhs_ weak_ent. Proof. rewrite predeq2E => x V; split. - case=> [? [[B ? <-] [? BsubV]]]; have: nbhs (f x) B by apply: open_nbhs_nbhs. + case=> [? [[B ? <-] ? BsubV]]; have: nbhs (f x) B by apply: open_nbhs_nbhs. move=> /nbhsP [W ? WsubB]; exists ((map_pair f) @^-1` W); first by exists W. by move=>??; exact/BsubV/WsubB. case=> W [V' entV' V'subW] /filterS; apply. have : nbhs (f x) to_set V' (f x) by apply/nbhsP; exists V'. -rewrite (@nbhsE U) => [[O [[openU Ofx Osub]]]]. +rewrite (@nbhsE U) => [[O [openU Ofx Osub]]]. (exists (f @^-1` O); repeat split => //); first by exists O => //. by move=> w ? ; apply: V'subW; exact: Osub. Qed. @@ -4324,7 +4338,7 @@ Qed. Lemma sup_ent_nbhs : @nbhs Tt Tt = nbhs_ sup_ent. Proof. rewrite predeq2E => x V; split. - rewrite /nbhs_of_open => [[? [[B + <-] [[W BW Wx] BV]]]] => /(_ W BW) []. + rewrite /nbhs_of_open => [[? [[B + <-] [W BW Wx] BV]]] => /(_ W BW) []. move=> F Fsup Weq; move: Weq Wx BW => <- Fx BF. case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]]. suff -> : V = setT by exists setT; apply: filterT; exact: sup_ent_filter. @@ -5607,7 +5621,7 @@ Lemma uniform_nbhs (f : fct_RestrictedUniformTopology) P: nbhs f P <-> (exists E, entourage E /\ [set h | forall y, A y -> E(f y, h y)] `<=` P). Proof. -split=> [[Q [[/= W oW <- /=] [Wf subP]]]|[E [entE subP]]]. +split=> [[Q [[/= W oW <- /=] Wf subP]]|[E [entE subP]]]. rewrite openE /= /interior in oW. case: (oW _ Wf) => ? [ /= E entE] Esub subW. exists E; split=> // h Eh; apply/subP/subW/Esub => /= [[u Au]]. @@ -6396,7 +6410,7 @@ Section SubspaceOpen. Lemma open_subspace1out (x : subspace A) : ~ A x -> open [set x]. Proof. move=> /nbhs_subspace_out E; have : nbhs x [set x] by rewrite /nbhs //= -E. -rewrite nbhsE => [[U [[]]]] oU Ux Usub; suff : U = [set x] by move=> <-. +rewrite nbhsE => [[U []]] oU Ux Usub; suff : U = [set x] by move=> <-. by rewrite eqEsubset; split => // t ->. Qed. @@ -6782,6 +6796,123 @@ Qed. End SubspaceWeak. +Definition separate_points_from_closed {I : Type} {T : topologicalType} + {U_ : I -> topologicalType} (f_ : forall i, T -> U_ i) := + forall (U : set T) x, + closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). + +(* A handy technique for embedding a space T into a product. The key interface + is 'separate_points_from_closed', which guarantees that the topologies + - T's native topology + - sup (weak f_i) - the sup of all the weak topologies of f_i + - weak (x => (f_1 x, f_2 x,...)) - the weak topology from the product space + are equivalent (the last equivalence seems to require accessible_space). +*) +Section product_embeddings. +Context {I : choiceType} {T : topologicalType} {U_ : I -> topologicalType}. +Variable (f_ : forall i, T -> U_ i). + +Hypothesis sepf : separate_points_from_closed f_. +Hypothesis ctsf : forall i, continuous (f_ i). + +Let weakT := @sup_topologicalType T I + (fun i => Topological.class (weak_topologicalType (f_ i))). + +Let PU := product_topologicalType U_. + +Local Notation sup_open := (@open weakT). +Local Notation "'weak_open' i" := + (@open (weak_topologicalType (f_ i))) (at level 0). +Local Notation natural_open := (@open T). + +Lemma weak_sep_cvg (F : set (set T)) (x : T) : + Filter F -> (F --> (x : T)) <-> (F --> (x : weakT)). +Proof. +move=> FF; split. + move=> FTx; apply/cvg_sup => i U. + have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. + case=> B [[C oC <- ?]] /filterS; apply; apply: FTx; rewrite /= nbhsE. + by exists (f_ i @^-1` C) => //; split => //; exact: open_comp. +move/cvg_sup => wiFx U; rewrite /= nbhs_simpl nbhsE => [[B [oB ?]]]. +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. +rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. +by move/forall2NP => /(_ z) [] // /contrapT. +Qed. + +Lemma weak_sep_nbhsE x : @nbhs T T x = @nbhs T weakT x. +Proof. +rewrite predeqE => U; split; move: U. + by have P := weak_sep_cvg x (nbhs_filter (x : weakT)); exact/P. +by have P := weak_sep_cvg x (nbhs_filter (x : T)); exact/P. +Qed. + +Lemma weak_sep_openE : @open T = @open weakT. +Proof. +rewrite predeqE => A; rewrite ?openE /interior. +by split => + z => /(_ z); rewrite weak_sep_nbhsE. +Qed. + +Definition join_product (x : T) : PU := f_ ^~ x. + +Lemma join_product_continuous : continuous join_product. +Proof. +suff : continuous (join_product : weakT -> PU). + by move=> cts x U => /cts; rewrite nbhs_simpl /= -weak_sep_nbhsE. +move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). +move=> i; move: x; apply/(@continuousP _ (weak_topologicalType _)) => A [B ? E]. +rewrite -E (_ : @^~ i = proj i) //. +have -> : join_product @^-1` (proj i @^-1` B) = f_ i @^-1` B by []. +apply: open_comp => // + _; rewrite /cvg_to => x U. +by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. +Qed. + +Local Notation prod_open := + (@open (subspace_topologicalType (range join_product))). + +Lemma join_product_open (A : set T) : open A -> + open ((join_product @` A) : set (subspace (range join_product))). +Proof. +move=> oA; rewrite openE => y /= [x Ax] jxy. +have [// | i nAfiy] := @sepf (~` A) x (open_closedC oA). +pose B : set PU := proj i @^-1` (~` closure (f_ i @` ~` A)). +apply: (@filterS _ _ _ (range join_product `&` B)). + move=> z [[w ?]] wzE Bz; exists w => //. + move: Bz; rewrite /B -wzE closureC; case=> K [oK KsubA] /KsubA. + have -> : proj i (join_product w) = f_ i w by []. + by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT. +apply: open_nbhs_nbhs; split; last by rewrite -jxy. +apply: openI; first exact: open_subspaceT. +apply: open_subspaceW; apply: open_comp; last exact/closed_openC/closed_closure. +by move=> + _; exact: proj_continuous. +Qed. + +Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product. +Proof. +move=> /accessible_closed_set1 cl1 x y; case: (eqVneq x y) => // xny _ _ jxjy. +have [] := (@sepf [set y] x (cl1 y)); first by exact/eqP. +move=> i P; suff : join_product x i != join_product y i by rewrite jxjy => /eqP. +apply/negP; move: P; apply: contra_not => /eqP; rewrite /join_product => ->. +by apply subset_closure; exists y. +Qed. + +Lemma join_product_weak : set_inj [set: T] join_product -> + @open T = @open (weak_topologicalType join_product). +Proof. +move=> inj; rewrite predeqE => U; split; first last. + by move=> [V ? <-]; apply open_comp => // + _; exact: join_product_continuous. +move=> /join_product_open/open_subspaceP [V [oU VU]]. +exists V => //; have := @f_equal _ _ (preimage join_product) _ _ VU. +rewrite !preimage_setI // !preimage_range !setIT => ->. +rewrite eqEsubset; split; last exact: preimage_image. +by move=> z [w Uw] /inj <- //; rewrite inE. +Qed. + +End product_embeddings. + Lemma continuous_compact {T U : topologicalType} (f : T -> U) A : {within A, continuous f} -> compact A -> compact (f @` A). Proof. @@ -6879,9 +7010,8 @@ split; first by move=> ? ?; near=> U; apply: continuous_subspaceT=> ?; exact. move=> + x => /(_ x)/near_powerset_filter_fromP. case; first by move=> ? ?; exact: continuous_subspaceW. move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U. - move: nbhsU; rewrite nbhsE => -[] W [[oW Wx WU]] /(_ W). - move/(_ (continuous_subspaceW WU wctsf)); apply => //. - by exists W; split. + move: nbhsU; rewrite nbhsE => -[] W [oW Wx WU] /(_ W). + by move/(_ (continuous_subspaceW WU wctsf)); apply => //; exists W. move/nbhs_singleton: nbhsU; move: x; apply/in_setP. by rewrite -continuous_open_subspace. Unshelve. end_near. Qed.