From 6e987e26bbd5f0ac7d66bbdc5116836a5bd7782b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 3 Mar 2026 20:08:22 +0900 Subject: [PATCH 1/6] set of limit points is closed --- CHANGELOG_UNRELEASED.md | 2 ++ theories/normedtype_theory/normed_module.v | 31 ++++++++++++++++++++++ 2 files changed, 33 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 30fef8c4f..771c59e0e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -78,6 +78,8 @@ - in `derive.v`: + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr` + lemmas `derivable0`, `derive0`, `is_derive0` +- in `normed_module.v`: + + lemmas `not_limit_point_set1`, `limit_point_closed` ### Changed diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 9ccf4583a..9184d699f 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1078,6 +1078,37 @@ move=> p q _ _ /=; apply: contraPP => /eqP. by rewrite neq_lt => /orP[] /arv /[swap] ->; rewrite ltxx. Qed. +Section limit_point_closed. +Context {R : archiRealFieldType}. +Implicit Types (A : set R) (a : R). + +Lemma not_limit_point_set1 A a : ~ limit_point A a -> + exists e : {posnum R}, ball a e%:num `&` A `<=` [set a]. +Proof. +move=> Ua; apply/not_existsP => aAa. +apply: Ua => /= V [e /= e0 aeV]. +have /nonsubset[/= x [[aex Ax] /eqP xa]] := aAa (PosNum e0). +by exists x; split => //; exact: aeV. +Qed. + +Lemma limit_point_closed A : closed (limit_point A). +Proof. +rewrite -openC openE/= => a /not_limit_point_set1[e AeAa]. +exists e%:num => //= b bae. +suff : b \notin limit_point A by rewrite notin_setE. +have {}bae : nbhs b (ball a e%:num). + have [->|ab] := eqVneq a b; first exact: nbhsx_ballx. + exists (Num.min `|b - a| (e%:num - `|b - a|)) => /=. + by rewrite lt_min/= normr_gt0 subr_eq0 eq_sym ab/= subr_gt0 distrC. + move=> x; rewrite /ball /ball_ /= lt_min => /andP[bxba bxe]. + by rewrite -(subrKA b) (le_lt_trans (ler_normD _ _))// -ltrBrDl (distrC a). +rewrite notin_setE => /limit_point_infinite_setP/(_ _ bae); apply. +exact: (sub_finite_set AeAa). +Qed. + +End limit_point_closed. +Arguments limit_point_closed {R} A. + Lemma limit_point_setD {R : archiRealFieldType} (A V : set R) a : finite_set V -> limit_point A a -> limit_point (A `\` V) a. Proof. From c7e4da8a950142bcdf47dd55cf9b563d0ca1162c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Mar 2026 18:08:50 +0900 Subject: [PATCH 2/6] generalization Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 5 ++++ theories/topology_theory/separation_axioms.v | 25 +++++++++++++++++++ theories/topology_theory/topology_structure.v | 10 ++++++++ 3 files changed, 40 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 771c59e0e..4e48f750a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -80,6 +80,11 @@ + lemmas `derivable0`, `derive0`, `is_derive0` - in `normed_module.v`: + lemmas `not_limit_point_set1`, `limit_point_closed` +- in `topology_structure.v`: + + lemma `limit_pointNE` + +- in `separation_axioms.v`: + + lemmas `limit_point_closed` ### Changed diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 9061ed845..7ea0e97a4 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -201,6 +201,31 @@ Arguments hausdorff_space : clear implicits. Arguments accessible_space : clear implicits. Arguments kolmogorov_space : clear implicits. +Lemma limit_point_closed {T : topologicalType} (A : set T) : + accessible_space T -> closed (limit_point A). +Proof. +move=> accT; rewrite -openC openE/= => a. +rewrite /setC/= limit_pointNE => -[X]. +rewrite nbhsE/= => -[U oaU UX] XAa. +rewrite /interior nbhsE/=. +exists U => // x Ux /=. +rewrite limit_pointNE. +have [xa|xneqa] := eqVneq x a. + exists U; rewrite xa; first exact: open_nbhs_nbhs. + by apply: subset_trans XAa; exact: setIS. +exists (U `&` [set~ a]). + apply: open_nbhs_nbhs; split. + apply: openI; first by case: oaU. + by rewrite openC; exact: accessible_closed_set1. + by split => //; exact/eqP. +apply: (@subset_trans _ (A `&` (X `&` [set~ a]))). + by apply: setIS; exact: setSI. +apply: (@subset_trans _ ([set a] `&` [set~ a])). + by rewrite setIA; exact: setSI. +by rewrite setICr. +Qed. +Arguments limit_point_closed {T} A. + Lemma subspace_hausdorff {T : topologicalType} (A : set T) : hausdorff_space T -> hausdorff_space (subspace A). Proof. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index ac7222837..af8024bf4 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -689,6 +689,16 @@ Proof. by rewrite limit_pointEnbhs; under eq_fun do rewrite meets_openr. Qed. Lemma subset_limit_point E : limit_point E `<=` closure E. Proof. by move=> t Et U tU; have [p [? ? ?]] := Et _ tU; exists p. Qed. +Lemma limit_pointNE A a : (~ limit_point A a) = + exists2 X : set T, nbhs a X & A `&` X `<=` [set a]. +Proof. +rewrite /limit_point/= -existsNE exists2E; apply: eq_exists => X/=. +rewrite not_implyE; congr and. +rewrite -forallNE; apply: eq_forall => x/=. +rewrite and3E not_andE orC -implyE; congr (_ -> _). +by rewrite -(propext (rwP negP)) not_notE -(propext (rwP eqP)). +Qed. + Definition isolated (A : set T) (x : T) := x \in A /\ exists2 V, nbhs x V & V `&` A = [set x]. From 36e69b727da24b15850567961d39d1ade829e6ec Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Mar 2026 18:11:03 +0900 Subject: [PATCH 3/6] rm --- theories/normedtype_theory/normed_module.v | 31 ---------------------- 1 file changed, 31 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 9184d699f..9ccf4583a 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1078,37 +1078,6 @@ move=> p q _ _ /=; apply: contraPP => /eqP. by rewrite neq_lt => /orP[] /arv /[swap] ->; rewrite ltxx. Qed. -Section limit_point_closed. -Context {R : archiRealFieldType}. -Implicit Types (A : set R) (a : R). - -Lemma not_limit_point_set1 A a : ~ limit_point A a -> - exists e : {posnum R}, ball a e%:num `&` A `<=` [set a]. -Proof. -move=> Ua; apply/not_existsP => aAa. -apply: Ua => /= V [e /= e0 aeV]. -have /nonsubset[/= x [[aex Ax] /eqP xa]] := aAa (PosNum e0). -by exists x; split => //; exact: aeV. -Qed. - -Lemma limit_point_closed A : closed (limit_point A). -Proof. -rewrite -openC openE/= => a /not_limit_point_set1[e AeAa]. -exists e%:num => //= b bae. -suff : b \notin limit_point A by rewrite notin_setE. -have {}bae : nbhs b (ball a e%:num). - have [->|ab] := eqVneq a b; first exact: nbhsx_ballx. - exists (Num.min `|b - a| (e%:num - `|b - a|)) => /=. - by rewrite lt_min/= normr_gt0 subr_eq0 eq_sym ab/= subr_gt0 distrC. - move=> x; rewrite /ball /ball_ /= lt_min => /andP[bxba bxe]. - by rewrite -(subrKA b) (le_lt_trans (ler_normD _ _))// -ltrBrDl (distrC a). -rewrite notin_setE => /limit_point_infinite_setP/(_ _ bae); apply. -exact: (sub_finite_set AeAa). -Qed. - -End limit_point_closed. -Arguments limit_point_closed {R} A. - Lemma limit_point_setD {R : archiRealFieldType} (A V : set R) a : finite_set V -> limit_point A a -> limit_point (A `\` V) a. Proof. From c175a0a28d77613e7305a0d0950ee087663916de Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Mar 2026 18:21:32 +0900 Subject: [PATCH 4/6] minor improvement --- theories/topology_theory/topology_structure.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index af8024bf4..ac8b72c07 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -693,10 +693,9 @@ Lemma limit_pointNE A a : (~ limit_point A a) = exists2 X : set T, nbhs a X & A `&` X `<=` [set a]. Proof. rewrite /limit_point/= -existsNE exists2E; apply: eq_exists => X/=. -rewrite not_implyE; congr and. -rewrite -forallNE; apply: eq_forall => x/=. -rewrite and3E not_andE orC -implyE; congr (_ -> _). -by rewrite -(propext (rwP negP)) not_notE -(propext (rwP eqP)). +rewrite not_implyE -forallNE; congr and; apply: eq_forall => t/=. +rewrite and3E not_andE (propext (rwP negP)) negbK implyE orC. +by rewrite -(propext (rwP eqP)). Qed. Definition isolated (A : set T) (x : T) := From 233c28a9c596a8956e9711cda67222bfc13655e9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 11 Mar 2026 10:52:13 +0900 Subject: [PATCH 5/6] renaming --- CHANGELOG_UNRELEASED.md | 2 +- theories/topology_theory/separation_axioms.v | 4 ++-- theories/topology_theory/topology_structure.v | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4e48f750a..9fa98a47d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,7 +81,7 @@ - in `normed_module.v`: + lemmas `not_limit_point_set1`, `limit_point_closed` - in `topology_structure.v`: - + lemma `limit_pointNE` + + lemma `not_limit_pointE` - in `separation_axioms.v`: + lemmas `limit_point_closed` diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 7ea0e97a4..b6ec16f63 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -205,11 +205,11 @@ Lemma limit_point_closed {T : topologicalType} (A : set T) : accessible_space T -> closed (limit_point A). Proof. move=> accT; rewrite -openC openE/= => a. -rewrite /setC/= limit_pointNE => -[X]. +rewrite /setC/= not_limit_pointE => -[X]. rewrite nbhsE/= => -[U oaU UX] XAa. rewrite /interior nbhsE/=. exists U => // x Ux /=. -rewrite limit_pointNE. +rewrite not_limit_pointE. have [xa|xneqa] := eqVneq x a. exists U; rewrite xa; first exact: open_nbhs_nbhs. by apply: subset_trans XAa; exact: setIS. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index ac8b72c07..c5c087cc1 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -689,7 +689,7 @@ Proof. by rewrite limit_pointEnbhs; under eq_fun do rewrite meets_openr. Qed. Lemma subset_limit_point E : limit_point E `<=` closure E. Proof. by move=> t Et U tU; have [p [? ? ?]] := Et _ tU; exists p. Qed. -Lemma limit_pointNE A a : (~ limit_point A a) = +Lemma not_limit_pointE A a : (~ limit_point A a) = exists2 X : set T, nbhs a X & A `&` X `<=` [set a]. Proof. rewrite /limit_point/= -existsNE exists2E; apply: eq_exists => X/=. From 552e6c74613045349d18befaca3d6430fbb5cfd1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Mar 2026 14:29:55 +0900 Subject: [PATCH 6/6] fix --- CHANGELOG_UNRELEASED.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9fa98a47d..42aa1376b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -78,8 +78,6 @@ - in `derive.v`: + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr` + lemmas `derivable0`, `derive0`, `is_derive0` -- in `normed_module.v`: - + lemmas `not_limit_point_set1`, `limit_point_closed` - in `topology_structure.v`: + lemma `not_limit_pointE`