From 9e257c1d75431e3dab40ba66f34265dd24925cf8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 3 Mar 2026 20:08:22 +0900 Subject: [PATCH 1/4] set of limit points is closed --- CHANGELOG_UNRELEASED.md | 3 +++ theories/normedtype_theory/normed_module.v | 31 ++++++++++++++++++++++ 2 files changed, 34 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0bf2951ee..b3e1f5134 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -72,6 +72,9 @@ - in `derive.v`: + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV` +- in `normed_module.v`: + + lemmas `not_limit_point_set1`, `limit_point_closed` + ### Changed - in `constructive_ereal.v`: fixed the infamous `%E` scope bug. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index d119bce20..317371b38 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1111,6 +1111,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 c09458607a51feecaaae87606b7e9f821e08a813 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Mar 2026 18:08:50 +0900 Subject: [PATCH 2/4] generalization Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 7 ++++-- theories/topology_theory/separation_axioms.v | 25 +++++++++++++++++++ theories/topology_theory/topology_structure.v | 10 ++++++++ 3 files changed, 40 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b3e1f5134..62dfcae47 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -72,8 +72,11 @@ - in `derive.v`: + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV` -- 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 6ac658b75ceebc66e507ddad8a5f6a0255e8c700 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Mar 2026 18:11:03 +0900 Subject: [PATCH 3/4] 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 317371b38..d119bce20 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1111,37 +1111,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 b25820847aaa6b5af522c50f8a8d308aeb69ef1b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 9 Mar 2026 18:21:32 +0900 Subject: [PATCH 4/4] 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) :=