From 3a5226bc31ed4c5604aa1756b0e574aaef617304 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 6 Nov 2024 23:47:19 +0900 Subject: [PATCH] duality between `closure` and `interior` (#1366) * duality between interior and closure --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 13 +++ classical/mathcomp_extra.v | 2 + theories/function_spaces.v | 5 +- theories/topology_theory/connected.v | 3 +- theories/topology_theory/topology_structure.v | 100 ++++++++++++++++-- 5 files changed, 110 insertions(+), 13 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1fe1fddcd..6e35b69d6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -96,7 +96,17 @@ + structure `NonNegSimpleFun` now inside a module `HBNNSimple` + lemma `cst_nnfun_subproof` has now a different statement + lemma `indic_nnfun_subproof` has now a different statement +- in `mathcomp_extra.v`: + + definition `idempotent_fun` +- in `topology_structure.v`: + + definitions `regopen`, `regclosed` + + lemmas `closure_setC`, `interiorC`, `closureU`, `interiorU`, + `closureEbigcap`, `interiorEbigcup`, + `closure_open_regclosed`, `interior_closed_regopen`, + `closure_interior_idem`, `interior_closure_idem` + +### Changed ### Renamed @@ -111,6 +121,9 @@ ### Deprecated +- in `topology_structure.v`: + + lemma `closureC` + ### Removed - in `lebesgue_integral.v`: diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 9fa2fa0a9..2c72f25ca 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -117,6 +117,8 @@ Arguments dfwith {I T} f i x. (* not yet backported *) (**********************) +Definition idempotent_fun (U : Type) (f : U -> U) := f \o f =1 f. + From mathcomp Require Import poly. Lemma deg_le2_ge0 (F : rcfType) (a b c : F) : diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 3d8991fc6..ec398b240 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -341,7 +341,7 @@ apply: (wiFx i); have /= -> := @nbhsE (weak_topology (f_ i)) x. exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); [split=>//|]. apply: open_comp; last by rewrite ?openC//; exact: closed_closure. by move=> + _; exact: (@weak_continuous _ _ (f_ i)). -rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. +rewrite -interiorC interiorEbigcup preimage_bigcup => z [V [oV]] VnB => /VnB. by move/forall2NP => /(_ z) [] // /contrapT. Qed. @@ -382,7 +382,8 @@ 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. + move: Bz; rewrite /B -wzE -interiorC interiorEbigcup. + 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. diff --git a/theories/topology_theory/connected.v b/theories/topology_theory/connected.v index 1a995a8ca..dd94ecae4 100644 --- a/theories/topology_theory/connected.v +++ b/theories/topology_theory/connected.v @@ -69,7 +69,8 @@ exists (fun i => if i is false then A `\` C else A `&` C); split. by apply: AF; rewrite BAC; exact/setIidPl. - by rewrite setDE -setIUr setUCl setIT. - split. - + rewrite setIC; apply/disjoints_subset; rewrite closureC => x [? ?]. + + rewrite setIC; apply/disjoints_subset. + rewrite -interiorC interiorEbigcup => x [? ?]. by exists C => //; split=> //; rewrite setDE setCI setCK; right. + apply/disjoints_subset => y -[Ay Cy]. rewrite -BAC BAD => /closureI[_]; move/closure_id : cD => <- Dy. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 095ed1add..29580b71a 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -27,8 +27,13 @@ From mathcomp Require Export filter. (* is convertible to G (globally A) *) (* finI_from D f == set of \bigcap_(i in E) f i where E is a *) (* finite subset of D *) -(* interior U == all of the points which are locally in U *) +(* interior U == all of the points which are locally in U, *) +(* i.e., the largest open set contained in U *) (* closure U == the smallest closed set containing U *) +(* regopen U == U is regular open, *) +(* i.e., equal to the interior of its closure *) +(* regclosed U == U is regular closed, *) +(* i.e., equal to the closure of its interior *) (* open_of_nbhs B == the open sets induced by neighborhoods *) (* nbhs_of_open B == the neighborhoods induced by open sets *) (* x^' == set of neighbourhoods of x where x is *) @@ -39,7 +44,6 @@ From mathcomp Require Export filter. (* type topologicalType *) (* discrete_space dscT == the discrete topology on T, provided *) (* a (dscT : discrete_space T) *) -(* *) (* ``` *) (* ### Factories *) (* ``` *) @@ -804,14 +808,6 @@ rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closure_subset AB). exact: (smallest_sub (@closed_closure _ _) (@subset_closure _ _)). Qed. -Lemma closureC E : - ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x. -Proof. -rewrite closureE setC_bigcap eqEsubset; split => t [U [? EU Ut]]. - by exists (~` U) => //; split; [exact: closed_openC|exact: subsetC]. -by rewrite -(setCK E); exists (~` U)=> //; split; [exact:open_closedC|exact:subsetC]. -Qed. - Lemma closure_id E : closed E <-> E = closure E. Proof. split=> [?|->]; last exact: closed_closure. @@ -820,6 +816,90 @@ Qed. End closure_lemmas. +Section regular_open_closed. +Variable T : topologicalType. + +Definition regopen (A : set T) := (closure A)^° = A. + +Definition regclosed (A : set T) := closure (A^°) = A. + +End regular_open_closed. + +Section closure_interior_lemmas. +Variable T : topologicalType. + +Lemma interiorC (A : set T) : (~` A)^° = ~` closure A. +Proof. +rewrite eqEsubset; split=> x; rewrite /closure /interior nbhsE /= -existsNE. + case=> U ? /disjoints_subset UA; exists U; rewrite not_implyE. + split; first exact/open_nbhs_nbhs. + by rewrite setIC UA; apply/set0P; rewrite eqxx. +case=> X; rewrite not_implyE nbhsE=> -[] -[] U xU UX AX0. +exists U => //; apply/(subset_trans UX)/disjoints_subset; rewrite setIC. +exact/eqP/negbNE/negP/set0P. +Qed. + +(* TODO: rename to closureC after removing the deprecated one *) +Lemma closure_setC (A : set T) : closure (~` A) = ~` A^°. +Proof. by apply: setC_inj; rewrite -interiorC !setCK. Qed. + +Lemma closureU (A B : set T) : closure (A `|` B) = closure A `|` closure B. +Proof. by apply: setC_inj; rewrite setCU -!interiorC -interiorI setCU. Qed. + +Lemma interiorU (A B : set T) : A^° `|` B^° `<=` (A `|` B)^°. +Proof. +by apply: subsetC2; rewrite setCU -!closure_setC setCU; exact: closureI. +Qed. + +Lemma closureEbigcap (A : set T) : + closure A = \bigcap_(x in [set C | closed C /\ A `<=` C]) x. +Proof. exact: closureE. Qed. + +Lemma interiorEbigcup (A : set T) : + A^° = \bigcup_(x in [set U | open U /\ U `<=` A]) x. +Proof. +apply: setC_inj; rewrite -closure_setC closureEbigcap setC_bigcup. +rewrite -[RHS](bigcap_image _ setC idfun) /=. +apply: eq_bigcapl; split => X /=. + by rewrite -openC -setCS setCK; exists (~` X)=> //; rewrite setCK. +by case=> Y + <-; rewrite closedC setCS. +Qed. + +Lemma interior_closed_regopen (A : set T) : closed A -> regopen A^°. +Proof. +move=> cA; rewrite /regopen eqEsubset; split=> x. + rewrite /closure [X in X -> _]/interior nbhsE => -[] U oxU UciA. + rewrite /interior nbhsE /=; exists U => //. + apply: (subset_trans UciA) => y /= yA. + apply: cA => B /yA; apply/subset_nonempty; apply: setSI. + exact: interior_subset. +rewrite {1}/interior nbhsE=> -[] U [] oU Ux UA. +rewrite {1}/interior nbhsE /=; exists U=> //. +have:= UA; rewrite open_subsetE// => /subset_trans; apply. +exact: subset_closure. +Qed. + +Lemma closure_open_regclosed (A : set T) : open A -> regclosed (closure A). +Proof. +rewrite /regclosed -(setCK A) openC => cCA. +rewrite closure_setC -[in RHS]interior_closed_regopen//. +by rewrite !(closure_setC, interiorC). +Qed. + +Lemma interior_closure_idem : @idempotent_fun (set T) (interior \o closure). +Proof. move=> ?; exact/interior_closed_regopen/closed_closure. Qed. + +Lemma closure_interior_idem : @idempotent_fun (set T) (closure \o interior). +Proof. move=> ?; exact/closure_open_regclosed/open_interior. Qed. + +End closure_interior_lemmas. + +Lemma closureC_deprecated (T : topologicalType) (E : set T) : + ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x. +Proof. by rewrite -interiorC interiorEbigcup. Qed. +#[deprecated(since="mathcomp-analysis 1.7.0", note="use `interiorC` and `interiorEbigcup` instead")] +Notation closureC := closureC_deprecated (only parsing). + Section DiscreteTopology. Section DiscreteMixin. Context {X : Type}.