New topology lemmas

CHANGELOG_UNRELEASED.md

@@ -11,8 +11,21 @@
   + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0`
   + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0`
 
+- in `function_spaces.v`:
+  + lemma `within_continuous_big`
+
+- in `nat_topology.v`:
+  + lemma `near_infty_leq`
+
+- in `num_topology.v`:
+  + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`,
+    `at_left_shift`, `at_right_shift`
+
 ### Changed
 
+- moved from `metric_structure.v` to `num_topology.v`: 
+  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`.
+
 ### Renamed
 
 ### Generalized

theories/topology_theory/function_spaces.v

@@ -1565,8 +1565,8 @@ End cartesian_closed.
 End currying.
 
 Section big_continuous.
-Context {U : topologicalType} {I : Type}.
-Variables (op : U -> U -> U) (x0 : U) (P : pred I).
+Context {U : topologicalType} {I : Type}
+  (op : U -> U -> U) (x0 : U) (P : pred I).
 Hypothesis cont_op : continuous (fun x : U * U => op x.1 x.2).
 
 Lemma cvg_big {T : Type} (F : set_system T) (r : seq I)
@@ -1598,6 +1598,12 @@ Proof.
 by move=> F_cont x; apply: cvg_big => // i /F_cont; exact.
 Qed.
 
+Lemma within_continuous_big {T : topologicalType} (A : set T) (r : seq I)
+    (F : I -> T -> U) :
+  (forall i, P i -> {within A, continuous (F i)}) ->
+  {within A, continuous (fun x => \big[op/x0]_(i <- r | P i) F i x)}.
+Proof. by move=> ? ?; exact: continuous_big. Qed.
+
 End big_continuous.
 
 Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=

theories/topology_theory/metric_structure.v

@@ -315,33 +315,6 @@ Unshelve. all: end_near. Qed.
 
 End cvg_nbhsP.
 
-Section cvg_at_right_left_dnbhs.
-Variables (R : realFieldType) (T : metricType R).
-
-Import metricType_numDomainType.
-
-Lemma cvg_at_right_left_dnbhs (f : R -> T) (p : R) (l : T) :
-  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
-  f x @[x --> p^'] --> l.
-Proof.
-move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
-have {fppl}[a /= a0 fppl] := fppl (at_right_proper_filter p) _ e0.
-have {fpnl}[b /= b0 fpnl] := fpnl (at_left_proper_filter p) _ e0.
-near=> t.
-have : t != p by near: t; exact: nbhs_dnbhs_neq.
-rewrite neq_lt => /orP[tp|pt].
-- apply: fpnl => //=; near: t.
-  exists (b / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-- apply: fppl =>//=; near: t.
-  exists (a / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-Unshelve. all: by end_near. Qed.
-
-End cvg_at_right_left_dnbhs.
-
 Section at_left_rightR.
 Variable (R : numFieldType).
 

theories/topology_theory/nat_topology.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order algebra all_classical.
 #[warning="-warn-library-file-internal-analysis"]
@@ -90,8 +90,17 @@ by rewrite /= -leq_divRL//; apply: Pn.
 Qed.
 
 Lemma near_inftyS (P : set nat) :
-  (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
-Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.
+  (\forall x \near \oo, P x.+1) -> (\forall x \near \oo, P x).
+Proof. by case=> N _ NPS; exists N.+1 => // [[]]; rewrite ?ltn0. Qed.
+
+Lemma near_infty_leq (P : set nat) :
+  (\forall n \near \oo, P n) <->
+  (\forall N \near \oo, forall n, (n >= N)%N -> P n).
+Proof.
+split => [[N _ /= NP]|].
+  by exists N => // n/= Nn m /(leq_trans Nn); exact: NP.
+by apply: filterS => N; exact.
+Qed.
 
 Section infty_nat.
 Local Open Scope nat_scope.

theories/topology_theory/num_topology.v

@@ -13,6 +13,9 @@ From mathcomp Require Import order_topology matrix_topology.
 (*                                                                            *)
 (******************************************************************************)
 
+Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+").
+Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-").
+
 Import Order.TTheory GRing.Theory Num.Theory.
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
@@ -146,11 +149,72 @@ Module Exports. HB.reexport. End Exports.
 End numFieldTopology.
 Import numFieldTopology.Exports.
 
-Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+").
-Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-").
+Lemma nbhsN {R : numFieldType} (x : R) : nbhs (- x) = -%R @ x.
+Proof.
+rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=.
+  by move=> ?; apply: xeA => //=; rewrite -opprD normrN.
+by rewrite -opprD normrN => ?; rewrite -[y]opprK; apply: xeA; rewrite /= opprK.
+Qed.
+
+Lemma cvg_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) (a : R)
+    (l : T) :
+  (f \o -%R) x @[x --> a] --> l <-> f x @[x --> (- a)] --> l.
+Proof. by rewrite nbhsN. Qed.
+
+Lemma withinN {R : numFieldType} (A : set R) (r : R) :
+  within A (nbhs (- r)) = - x @[x --> within (-%R @` A) (nbhs r)].
+Proof.
+rewrite eqEsubset /=; split; move=> E /= [e e0 reE]; exists e => //.
+  move=> s rse sA; apply: reE; last by rewrite memNE opprK.
+  by rewrite /= opprK addrC distrC.
+move=> s res rs; rewrite -(opprK s); apply: reE; last by rewrite -memNE.
+by rewrite /= opprK -normrN opprD.
+Qed.
+
+Lemma nearN {R : numFieldType} (x : R) (P : R -> Prop) :
+  (\forall y \near - x, P y) <-> \near x, P (- x).
+Proof. by rewrite -[X in X <-> _]near_simpl nbhsN. Qed.
+
+Lemma nbhsNimage {R : numFieldType} (x : R) :
+  nbhs (- x) = [set -%R @` A | A in nbhs x].
+Proof.
+rewrite nbhsN /fmap/=; under eq_set => A do rewrite preimageEinv//= inv_oppr.
+by rewrite (eq_imageK opprK opprK).
+Qed.
+
+Lemma openN {R : numFieldType} (A : set R) : open A -> open [set - x | x in A].
+Proof.
+move=> Aop; rewrite openE => _ [x /Aop x_A <-].
+by rewrite /interior nbhsNimage; exists A.
+Qed.
+
+Lemma closedN (R : numFieldType) (A : set R) :
+  closed A -> closed [set - x | x in A].
+Proof.
+move=> Acl x clNAx.
+suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK.
+move=> B oppx_B; have : [set - x | x in A] `&` [set - x | x in B] !=set0.
+  by apply: clNAx; rewrite -[x]opprK nbhsNimage; exists B.
+move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y).
+by split; [rewrite -oppzey opprK|rewrite -opptey opprK].
+Qed.
+
+Lemma dnbhsN {R : numFieldType} (r : R) :
+  (- r)%R^' = (fun A => -%R @` A) @` r^'.
+Proof.
+apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
+  exists (-%R @` A).
+    exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
+    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
+  rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
+  by rewrite opprK.
+exists e => //= x/=; rewrite -opprD normrN => axe xa.
+exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
+by rewrite opprK.
+Qed.
 
 Section at_left_right.
-Variable R : numFieldType.
+Context {R : numFieldType}.
 
 Definition at_left (x : R) := within (fun u => u < x) (nbhs x).
 Definition at_right (x : R) := within (fun u => x < u) (nbhs x).
@@ -241,6 +305,54 @@ split=> [pPf e|ex_notPx].
   by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl.
 Unshelve. all: by end_near. Qed.
 
+Lemma at_rightD x a : (x + a)^'+ = (y + a @[y --> x^'+]).
+Proof.
+apply/seteqP; split=> P /=.
+- move=> [/= r r0 xarP].
+  exists r => // y bxy x_lt_y.
+  apply: xarP => /=.
+  + by rewrite (addrC y) addrKA.
+  + by rewrite ltrD2r.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxay xDa_lt_y.
+  rewrite -(subrK a y).
+  apply: br_sub => /=.
+  + by rewrite opprB addrA.
+  + by rewrite ltrBrDr.
+Qed.
+
+Lemma at_leftD x a : (x + a)^'- = (y + a @[y --> x^'-]).
+Proof.
+apply/seteqP; split=> P /=.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxy x_lt_y.
+  apply: br_sub => /=.
+  + by rewrite (addrC y) addrKA.
+  + by rewrite ltrD2r.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxay xDa_lt_y.
+  rewrite -(subrK a y).
+  apply: br_sub => /=.
+  + by rewrite opprB addrA.
+  + by rewrite ltrBlDr.
+Qed.
+
+Lemma near_at_rightD x a (P : set R) :
+  (\forall y \near (x + a)^'+, P y) = (\forall y \near x^'+, P (y + a)).
+Proof. by rewrite at_rightD near_map. Qed.
+
+Lemma near_at_leftD x a (P : set R) :
+  (\forall y \near (x + a)^'-, P y) = (\forall y \near x^'-, P (y + a)).
+Proof. by rewrite at_leftD near_map. Qed.
+
+Lemma at_left_shift (T : Type) x a (f : R -> T) :
+  (f @ (x + a)^'-) = (f (y + a) @[y --> x^'-]).
+Proof. by rewrite at_leftD. Qed.
+
+Lemma at_right_shift (T : Type) x a (f : R -> T) :
+  (f @ (x + a)^'+) = (f (y + a) @[y --> x^'+]).
+Proof. by rewrite at_rightD. Qed.
+
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.
@@ -252,6 +364,16 @@ Notation "x ^'+" := (at_right x) : classical_set_scope.
 #[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
   (apply: at_left_proper_filter) : typeclass_instances.
 
+Lemma cvg_at_right_left_dnbhs (R : realFieldType) (T : topologicalType)
+    (f : R -> T) (p : R) (l : T) :
+  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l.
+Proof.
+move=> + + U Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
+rewrite !near_withinE !near_nbhs => lf rf.
+apply: filter_app lf; apply: filter_app rf.
+by near=> t => xlt xgt /lt_total/orP[|].
+Unshelve. all: by end_near. Qed.
+
 Lemma left_right_continuousP {R : realFieldType} {T : topologicalType}
     (f : R -> T) x :
   f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.
@@ -314,70 +436,6 @@ have : inf X <= inf X - f%:num by exact: ge_inf.
 by apply/negP; rewrite -ltNge; rewrite ltrBlDr ltrDl.
 Qed.
 
-Lemma nbhsN {R : numFieldType} (x : R) : nbhs (- x) = -%R @ x.
-Proof.
-rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=.
-  by move=> ?; apply: xeA => //=; rewrite -opprD normrN.
-by rewrite -opprD normrN => ?; rewrite -[y]opprK; apply: xeA; rewrite /= opprK.
-Qed.
-
-Lemma cvg_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) (a : R)
-    (l : T) :
-  (f \o -%R) x @[x --> a] --> l <-> f x @[x --> (- a)] --> l.
-Proof. by rewrite nbhsN. Qed.
-
-Lemma nbhsNimage {R : numFieldType} (x : R) :
-  nbhs (- x) = [set -%R @` A | A in nbhs x].
-Proof.
-rewrite nbhsN /fmap/=; under eq_set => A do rewrite preimageEinv//= inv_oppr.
-by rewrite (eq_imageK opprK opprK).
-Qed.
-
-Lemma nearN {R : numFieldType} (x : R) (P : R -> Prop) :
-  (\forall y \near - x, P y) <-> \near x, P (- x).
-Proof. by rewrite -[X in X <-> _]near_simpl nbhsN. Qed.
-
-Lemma openN {R : numFieldType} (A : set R) : open A -> open [set - x | x in A].
-Proof.
-move=> Aop; rewrite openE => _ [x /Aop x_A <-].
-by rewrite /interior nbhsNimage; exists A.
-Qed.
-
-Lemma closedN (R : numFieldType) (A : set R) :
-  closed A -> closed [set - x | x in A].
-Proof.
-move=> Acl x clNAx.
-suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK.
-move=> B oppx_B; have : [set - x | x in A] `&` [set - x | x in B] !=set0.
-  by apply: clNAx; rewrite -[x]opprK nbhsNimage; exists B.
-move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y).
-by split; [rewrite -oppzey opprK|rewrite -opptey opprK].
-Qed.
-
-Lemma dnbhsN {R : numFieldType} (r : R) :
-  (- r)%R^' = (fun A => -%R @` A) @` r^'.
-Proof.
-apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
-  exists (-%R @` A).
-    exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
-    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
-  rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
-  by rewrite opprK.
-exists e => //= x/=; rewrite -opprD normrN => axe xa.
-exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
-by rewrite opprK.
-Qed.
-
-Lemma withinN {R : numFieldType} (A : set R) (r : R) :
-  within A (nbhs (- r)) = - x @[x --> within (-%R @` A) (nbhs r)].
-Proof.
-rewrite eqEsubset /=; split; move=> E /= [e e0 reE]; exists e => //.
-  move=> s rse sA; apply: reE; last by rewrite memNE opprK.
-  by rewrite /= opprK addrC distrC.
-move=> s res rs; rewrite -(opprK s); apply: reE; last by rewrite -memNE.
-by rewrite /= opprK -normrN opprD.
-Qed.
-
 Lemma in_continuous_mksetP {T : realFieldType} {U : nbhsType}
     (i : interval T) (f : T -> U) :
   {in i, continuous f} <-> {in [set` i], continuous f}.