Merge pull request #1776 from affeldt-aist/fixes_1775

isolated points

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -71,6 +71,23 @@
   + lemmas `nondecreasing_measurable`, `nonincreasing_measurable`
 - in `subspace_topology.v`:
   + definition `from_subspace`
+- in `topology_structure.v`:
+  + definition `isolated`
+  + lemma `isolatedS`
+  + lemma `disjoint_isolated_limit_point`
+  + lemma `closure_isolated_limit_point`
+
+- in `separation_axioms.v`:
+  + lemma `perfectP`
+
+- in `cardinality.v`:
+  + lemmas `finite_setX_or`, `infinite_setX`
+  + lemmas `infinite_prod_rat`, ``card_rat2`
+
+- in `normed_module.v`:
+  + lemma `open_subball_rat`
+  + fact `isolated_rat_ball`
+  + lemma `countable_isolated`
 
 ### Changed
 
@@ -121,6 +138,9 @@
 
 ### Deprecated
 
+- in `topology_structure.v`:
+  + lemma `closure_limit_point` (use `closure_limit_point_isolated` instead)
+
 ### Removed
 
 - in `lebesgue_stieltjes_measure.v`:

classical/cardinality.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
@@ -632,6 +632,21 @@ Proof. by apply: subset_card_le; rewrite setDE; apply: subIset; left. Qed.
 Lemma finite_image T T' A (f : T -> T') : finite_set A -> finite_set (f @` A).
 Proof. exact/card_le_finite/card_image_le. Qed.
 
+Lemma finite_setX_or T T' (A : set T) (B : set T') :
+  finite_set (A `*` B) -> finite_set A \/ finite_set B.
+Proof.
+have [->|/set0P[a Aa]] := eqVneq A set0; first by left.
+have /sub_finite_set : [set a] `*` B `<=` A `*` B by move=> x/= [] -> ?; split.
+move => /[apply]/(finite_image snd); rewrite (_ : _ @` _ = B); first by right.
+by apply/seteqP; split=> [b [[? ?] [? ?] <-//]|b ?]/=; exists (a, b).
+Qed.
+
+Lemma infinite_setX {T} {A B : set T} :
+  infinite_set A -> infinite_set B -> infinite_set (A `*` B).
+Proof.
+by move=> iA iB; have /not_orP := conj iA iB; exact/contra_not/finite_setX_or.
+Qed.
+
 Lemma finite_set1 T (x : T) : finite_set [set x].
 Proof.
 elim/Pchoice: T => T in x *.
@@ -1099,9 +1114,7 @@ Lemma infinite_nat : ~ finite_set [set: nat].
 Proof. exact/infiniteP/card_lexx. Qed.
 
 Lemma infinite_prod_nat : infinite_set [set: nat * nat].
-Proof.
-by apply/infiniteP/pcard_leTP/injPex; exists (pair 0%N) => // m n _ _ [].
-Qed.
+Proof. by rewrite -setXTT; apply: infinite_setX; exact: infinite_nat. Qed.
 
 Lemma card_nat2 : [set: nat * nat] #= [set: nat].
 Proof. exact/eq_card_nat/infinite_prod_nat/countableP. Qed.
@@ -1117,6 +1130,12 @@ Qed.
 Lemma card_rat : [set: rat] #= [set: nat].
 Proof. exact/eq_card_nat/infinite_rat/countableP. Qed.
 
+Lemma infinite_prod_rat : infinite_set [set: rat * rat].
+Proof. by rewrite -setXTT; apply: infinite_setX; exact: infinite_rat. Qed.
+
+Lemma card_rat2 : ([set: rat * rat] #= [set: nat])%card.
+Proof. exact/eq_card_nat/infinite_prod_rat/countableP. Qed.
+
 Lemma choicePcountable {T : choiceType} : countable [set: T] ->
   {T' : countType | T = T' :> Type}.
 Proof.

classical/classical_sets.v

@@ -1,7 +1,7 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg matrix finmap ssrnum.
-From mathcomp Require Import ssrint interval.
+From mathcomp Require Import ssrint rat interval.
 From mathcomp Require Import mathcomp_extra boolp wochoice.
 
 (**md**************************************************************************)

theories/function_spaces.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
@@ -1218,8 +1218,7 @@ have C : compact R.
   by apply: tychonoff => x; rewrite -precompactE; move: ptwsPreW; exact.
 apply: (subclosed_compact _ C); first exact: closed_closure.
 have WsubR : (fW @` W) `<=` R.
-  move=> f Wf x; rewrite /R /K closure_limit_point; left.
-  by case: Wf => i ? <-; exists i.
+  by move=> f [i Wi <-] x; rewrite /K; apply: subset_closure; exists i.
 rewrite closureE; apply: smallest_sub (compact_closed _ C) WsubR.
 exact: hausdorff_product.
 Qed.

theories/normedtype_theory/normed_module.v

@@ -2088,6 +2088,85 @@ apply: filterS => e xeA y exy; apply: xeA.
 by rewrite -ball_normE/= in exy; exact: ltW.
 Qed.
 
+Lemma open_subball_rat {R : realType} (S : set R) x : open S -> x \in S ->
+  exists c r, let B : set R := ball (@ratr R c) (ratr r) in x \in B /\ B `<=` S.
+Proof.
+move=> oS /set_mem/(open_subball oS)[r/= r0 rS].
+have [y yxr] : exists y, ball x (r / 4) (ratr y).
+  suff : ball x (r / 4) `&` range ratr !=set0.
+    by move=> [/= _ []] /[swap] -[y _ <-]; exists y.
+  apply: dense_rat; last by apply: ball_open; rewrite divr_gt0.
+  by exists x; apply: ballxx; rewrite divr_gt0.
+have [q /andP[rq qr]] : exists q, r / 4 < ratr q < r / 2.
+  have : ball (r / 3) (r / 12) `&` range ratr !=set0.
+    apply: dense_rat; last by apply: ball_open; rewrite divr_gt0.
+    by exists (r / 3); apply: ballxx; rewrite divr_gt0.
+  move=> [/= _ []] /[swap] -[z _ <-].
+  rewrite ball_itv/= in_itv/= => /andP[rz zr]; exists z; apply/andP; split.
+  - rewrite (le_lt_trans _ rz)// -mulrBr ler_pM2l// -(@ler_pM2l _ 12)//.
+    rewrite mulrBr divff// (@natrM _ 3 4) -mulrA divff// mulr1.
+    by rewrite mulrAC divff// mul1r -lerBlDr opprK natr1.
+  - rewrite (lt_le_trans zr)// -mulrDr ler_pM2l// -(@ler_pM2l _ 12)//.
+    rewrite mulrDr divff// (@natrM _ 3 4) mulrAC divff// mul1r.
+    by rewrite natr1 (@natrM _ 2 2) -!mulrA divff// mulr1 -natrM ler_nat.
+have [yqxr xrS] : ball (@ratr R y) (ratr q) `<=` ball x r /\ ball x r `<=` S.
+  split => [z yqz|z /rat_in_itvoo[p]].
+  - rewrite /ball/= -(subrK (ratr y) x) -(addrA _ (ratr y)).
+    rewrite (le_lt_trans (ler_normD _ _))// (splitr r) ltrD//.
+      by apply: le_ball yxr; rewrite ler_pM2l// lef_pV2 ?posrE// ler_nat.
+    by rewrite (lt_trans yqz).
+  - rewrite in_itv/= => /andP[xzp pr]; apply: (rS (ratr p)) => //=.
+    + by rewrite sub0r normrN gtr0_norm// (le_lt_trans _ xzp).
+    + exact: le_lt_trans xzp.
+exists y, q; split; last exact: subset_trans xrS.
+exact/mem_set/ball_sym/(le_ball _ yxr)/ltW.
+Qed.
+
+Section countable_isolated.
+Context {R : realType}.
+Variable S : set R.
+
+Fact isolated_rat_ball (x : R) : isolated S x -> exists cr,
+  let B : set R := ball (@ratr R cr.1) (ratr cr.2) in
+  x \in B /\ (forall y : R, isolated S y -> y \in B -> x = y).
+Proof.
+move=> Sx.
+have [e Sxe] : exists e : {posnum R},
+    forall y : R, isolated S y -> y \in (ball x e%:num : set R) -> x = y.
+  case: Sx => [xS/= [V xV /seteqP[VSx _]]].
+  have [e /= e0 exV] : \forall e \near 0^'+, ball x e `<=` V°.
+    apply: open_subball; first exact: open_interior.
+    by move/nbhs_interior : xV; exact: nbhs_singleton.
+  have e20 : 0 < e / 2 by rewrite divr_gt0.
+  exists (PosNum e20) => y [Sy [/= U yU USy /set_mem xey]].
+  apply/eqP/negPn/negP => xy.
+  suff : (V `&` S) y by move/VSx/esym; exact/eqP.
+  split => //; last exact/set_mem.
+  apply: interior_subset; apply: exV xey => //.
+  by rewrite /ball_/= sub0r normrN gtr0_norm// gtr_pMr// invf_lt1// ltr1n.
+have [c [r [xcr crxe]]] : exists c r,
+  let B : set R := ball (@ratr R c) (ratr r) in x \in B /\ B `<=` ball x e%:num.
+  by apply: open_subball_rat; [exact: ball_open|exact/mem_set/ballxx].
+by exists (c, r); split=> //= y /Sxe /[!inE] /[swap] /crxe /[swap] /[apply].
+Qed.
+
+Lemma countable_isolated : countable (isolated S).
+Proof.
+apply/pcard_injP => /=.
+pose g r := if pselect (isolated S r) is left H then
+  sval (cid (isolated_rat_ball H)) else 0.
+have /card_bijP[h /bij_inj injh] := card_rat2.
+exists (set_val \o h \o to_setT \o g) => x y /set_mem xS /set_mem yS /=.
+rewrite /= /g; case: pselect => // xS'; case: pselect => // yS'.
+case: cid => //= [ar [xar Nxar]]{xS'}; case: cid => //= [bd [ybd Nybd]]{yS'} ab.
+have /injh/(congr1 (fun x => \val x)) : h (to_setT ar) = h (to_setT bd).
+  move: (h (to_setT ar)) (h (to_setT bd)) ab => [n nT] [m mT].
+  by rewrite !set_valE/= => ->; congr exist.
+by rewrite -inv_to_setT !funK ?inE// => {}ab; apply: Nxar => //; rewrite ab.
+Qed.
+
+End countable_isolated.
+
 Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R}
     (K : set M) z : closed K -> ~ K z ->
   \forall d \near 0^'+, closed_ball z d `&` K = set0.

theories/normedtype_theory/vitali_lemma.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval.
-From mathcomp Require Import archimedean.
+From mathcomp Require Import archimedean rat.
 From mathcomp Require Import boolp classical_sets functions cardinality.
 From mathcomp Require Import set_interval interval_inference ereal reals.
 From mathcomp Require Import topology function_spaces tvs num_normedtype.

theories/topology_theory/num_topology.v

@@ -149,7 +149,8 @@ Lemma closure_sup (R : realType) (A : set R) :
   A !=set0 -> has_ubound A -> closure A (sup A).
 Proof.
 move=> A0 ?; have [|AsupA] := pselect (A (sup A)); first exact: subset_closure.
-rewrite closure_limit_point; right => U /nbhs_ballP[_ /posnumP[e]] supAeU.
+rewrite closure_isolated_limit_point.
+right => U /nbhs_ballP[_ /posnumP[e]] supAeU.
 suff [x [Ax /andP[sAex xsA]]] : exists x, A x /\ sup A - e%:num < x < sup A.
   exists x; split => //; first by rewrite lt_eqF.
   apply supAeU; rewrite /ball /= ltr_distl (addrC x e%:num) -ltrBlDl sAex.

theories/topology_theory/separation_axioms.v

@@ -1078,6 +1078,17 @@ Implicit Types (T : topologicalType).
 
 Definition perfect_set {T} (A : set T) := closed A /\ limit_point A = A.
 
+Lemma perfectP {T} (A : set T) :
+  perfect_set A <-> closed A /\ isolated A = set0.
+Proof.
+split=> [[cA limA]|[cA isoA]]; have := closure_isolated_limit_point A.
+- move=> /(congr1 (fun x => x `\` limit_point A)).
+  rewrite setUDK.
+    by rewrite limA -(closure_id A).1// setDv.
+  by apply/disj_setPS; rewrite disj_set_sym disjoint_isolated_limit_point.
+- by rewrite isoA set0U -(closure_id A).1.
+Qed.
+
 Lemma perfectTP {T} : perfect_set [set: T] <-> forall x : T, ~ open [set x].
 Proof.
 split.

theories/topology_theory/topology_structure.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap all_classical.
 From mathcomp Require Export filter.
@@ -40,6 +40,7 @@ From mathcomp Require Export filter.
 (*                      x^' == set of neighbourhoods of x where x is          *)
 (*                             excluded (a "deleted neighborhood")            *)
 (*            limit_point E == the set of limit points of E                   *)
+(*               isolated A == the set of isolated points of A                *)
 (*                  dense S == the set (S : set T) is dense in T, with T of   *)
 (*                             type topologicalType                           *)
 (*           continuousType == type of continuous functions                   *)
@@ -687,12 +688,43 @@ 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 closure_limit_point E : closure E = E `|` limit_point E.
+Definition isolated (A : set T) (x : T) :=
+  x \in A /\ exists2 V, nbhs x V & V `&` A = [set x].
+
+Lemma isolatedS (A : set T) : isolated A `<=` A.
+Proof. by move=> x [/set_mem]. Qed.
+
+Lemma disjoint_isolated_limit_point (A : set T) :
+  [disjoint isolated A & limit_point A].
+Proof.
+apply/disj_setPS => t [[At [V tV]]] /[swap].
+move/(_ _ tV) => [x [xt Ax Vx]].
+have /[swap] -> : [set x] `<=` V `&` A by move=> ? ->; split.
+move/subset_set1 => [/seteqP[/(_ _ erefl)//]|].
+by move=> /seteqP[_ /(_ _ erefl)/=]; apply/eqP; rewrite eq_sym.
+Qed.
+
+Lemma closure_isolated_limit_point (A : set T) :
+  closure A = isolated A `|` limit_point A.
+Proof.
+apply/seteqP; split=> [t At0|t [|]].
+- rewrite /setU/= -implyNp => /not_andP[tA U /At0[x [Ux Ax]]|+ U tU].
+    by exists x; split => //; contra: tA => <-; exact/mem_set.
+  move/forall2NP => /(_ U)[//|/seteqP/not_andP[|]].
+    by contra => H x [Ux Ax]; apply/eqP/negPn/negP => /H /(_ Ax).
+  have [At tUA|At _] := pselect (A t).
+    by absurd: tUA => _ ->; split => //; exact: nbhs_singleton.
+  have [x [Ax Ux]] := At0 _ tU.
+  by exists x; split => //; contra: At => <-.
+- by move/isolatedS; exact: subset_closure.
+- exact: subset_limit_point.
+Qed.
+
+Lemma __deprecated__closure_limit_point E : closure E = E `|` limit_point E.
 Proof.
-rewrite predeqE => t; split => [cEt|]; last first.
+apply/seteqP; split => [|x]; last first.
   by case; [exact: subset_closure|exact: subset_limit_point].
-have [?|Et] := pselect (E t); [by left|right=> U tU; have [p []] := cEt _ tU].
-by exists p; split => //; apply/eqP => pt; apply: Et; rewrite -pt.
+by rewrite closure_isolated_limit_point => x [/isolatedS|]; [left|right].
 Qed.
 
 Definition closed (D : set T) := closure D `<=` D.
@@ -749,6 +781,8 @@ Lemma closed_closure (A : set T) : closed (closure A).
 Proof. by move=> p clclAp B /nbhs_interior /clclAp [q [clAq /clAq]]. Qed.
 
 End Closed.
+#[deprecated(since="mathcomp-analysis 1.15.0", note="use `closure_limit_point_isolated` instead")]
+Notation closure_limit_point := __deprecated__closure_limit_point (only parsing).
 
 Lemma closed_comp {T U : topologicalType} (f : T -> U) (D : set U) :
   {in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D).