From b3ec54368fc58f98c97a9c42fea50c9ae648de6f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 24 Oct 2026 17:08:48 +0900 Subject: [PATCH 1/3] rm \near _, _ notation --- CHANGELOG_UNRELEASED.md | 5 ++ analysis_stdlib/Rstruct_topology.v | 3 +- classical/filter.v | 31 ++----- theories/derive.v | 8 +- theories/ereal.v | 15 ++-- theories/ftc.v | 6 +- theories/landau.v | 3 +- theories/normedtype_theory/ereal_normedtype.v | 13 +-- theories/normedtype_theory/normed_module.v | 87 ++++++++++--------- theories/normedtype_theory/num_normedtype.v | 14 +-- .../pseudometric_normed_Zmodule.v | 36 ++++---- theories/topology_theory/compact.v | 5 +- theories/topology_theory/metric_structure.v | 7 +- theories/topology_theory/num_topology.v | 5 +- .../one_point_compactification.v | 4 +- .../topology_theory/pseudometric_structure.v | 4 +- theories/topology_theory/topology_structure.v | 25 +++--- theories/topology_theory/uniform_structure.v | 5 +- 18 files changed, 138 insertions(+), 138 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4181add17c..c125ad66d6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -386,6 +386,11 @@ - in `radon_nikodym.v`: + notation `induced` (deprecated since 1.15.0) +- in `filter.v`: + + notation `\near x, P x` + + notation `\near x & y, P x y` + + lemma `near_nbhs` + ### Infrastructure ### Misc diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index ce7fe4028d..c155d7a87e 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -20,7 +20,6 @@ From mathcomp Require exp. (* The following line is for RcosE, PIE and RsinE. *) From mathcomp Require trigonometry_functions. -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -88,7 +87,7 @@ by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP. Qed. Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) : - nbhs (f x) P -> continuity_pt f x -> \near x, P (f x). + nbhs (f x) P -> continuity_pt f x -> \forall x0 \near x, P (f x0). Proof. by move=> Lf /continuity_pt_cvg; apply. Qed. End analysis_struct. diff --git a/classical/filter.v b/classical/filter.v index e56e6c030d..878c6897df 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -147,12 +147,10 @@ From mathcomp Require Import boolp classical_sets functions wochoice (* Prefer this notation when the *) (* statement forall x, P x does not stand *) (* alone. *) -(* \near x, P x := \forall y \near x, P y. *) (* {near F & G, P} == same as {near H, P}, where H is the *) (* product of the filters F and G *) (* \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y} *) (* \forall x & y \near F, P x y == same as before, with G = F *) -(* \near x & y, P x y := \forall z \near x & t \near y, P x y *) (* x \is_near F == x belongs to a set P : in_filter F *) (* ``` *) (* *) @@ -196,9 +194,6 @@ Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }"). Reserved Notation "'\forall' x '\near' x_0 , P" (at level 200, x name, P at level 200, format "'\forall' x '\near' x_0 , P"). -Reserved Notation "'\near' x , P" - (at level 200, x at level 99, P at level 200, - format "'\near' x , P", only parsing). Reserved Notation "{ 'near' x & y , P }" (at level 0, format "{ 'near' x & y , P }"). Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" @@ -207,9 +202,6 @@ Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" Reserved Notation "'\forall' x & y '\near' z , P" (at level 200, x name, y name, P at level 200, format "'\forall' x & y '\near' z , P"). -Reserved Notation "'\near' x & y , P" - (at level 200, x, y at level 99, P at level 200, - format "'\near' x & y , P", only parsing). (*Reserved Notation "[ 'filter' 'of' x ]" (format "[ 'filter' 'of' x ]").*) Reserved Notation "F `=>` G" (at level 70, format "F `=>` G"). Reserved Notation "F --> G" (at level 70, format "F --> G"). @@ -289,14 +281,12 @@ End Near. Notation "{ 'near' x , P }" := (@prop_near1 _ _ x _ (inPhantom P)) : type_scope. Notation "'\forall' x '\near' x_0 , P" := {near x_0, forall x, P} : type_scope. -Notation "'\near' x , P" := (\forall x \near x, P) : type_scope. Notation "{ 'near' x & y , P }" := (@prop_near2 _ _ _ _ x y _ (inPhantom P)) : type_scope. Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" := {near x_0 & y_0, forall x y, P} : type_scope. Notation "'\forall' x & y '\near' z , P" := {near z & z, forall x y, P} : type_scope. -Notation "'\near' x & y , P" := (\forall x \near x & y \near y, P) : type_scope. Arguments prop_near1 : simpl never. Arguments prop_near2 : simpl never. @@ -401,11 +391,7 @@ Arguments cvgP {T F} l. Arguments dvgP {T F}. Lemma nbhs_nearE {U} {T : filteredType U} (x : T) (P : set U) : - nbhs x P = \near x, P x. -Proof. by []. Qed. - -Lemma near_nbhs {U} {T : filteredType U} (x : T) (P : set U) : - (\forall x \near nbhs x, P x) = \near x, P x. + nbhs x P = \forall x0 \near x, P x0. Proof. by []. Qed. Lemma near2_curry {U V} (F : set_system U) (G : set_system V) (P : U -> set V) : @@ -424,7 +410,7 @@ Lemma filter_of_nearI (X : Type) (fX : filteredType X) Proof. by []. Qed. Module Export NearNbhs. -Definition near_simpl := (@near_nbhs, @nbhs_nearE, filter_of_nearI). +Definition near_simpl := (filter_of_nearI). Ltac near_simpl := rewrite ?near_simpl. End NearNbhs. @@ -525,7 +511,7 @@ Lemma filter_nbhsT {T : Type} (F : set_system T) : Proof. by move=> FF; apply: filterT. Qed. #[global] Hint Resolve filter_nbhsT : core. -Lemma nearT {T : Type} (F : set_system T) : Filter F -> \near F, True. +Lemma nearT {T : Type} (F : set_system T) : Filter F -> \forall _ \near F, True. Proof. by move=> FF; apply: filterT. Qed. #[global] Hint Resolve nearT : core. @@ -693,10 +679,9 @@ Lemma in_filter_from {I T : Type} (D : set I) (B : I -> set T) (i : I) : Proof. by exists i. Qed. Lemma in_nearW {T : Type} (F : set_system T) (P : T -> Prop) (S : set T) : - Filter F -> F S -> {in S, forall x, P x} -> \near F, P F. + Filter F -> F S -> {in S, forall x, P x} -> \forall x \near F, P x. Proof. -move=> FF FS SP; rewrite -nbhs_nearE. -by apply: (@filterS _ F _ S) => // x /mem_set /SP. +by move=> FF FS SP; apply: (@filterS _ F _ S) => // x /mem_set /SP. Qed. Lemma near_andP {T : Type} F (b1 b2 : T -> Prop) : Filter F -> @@ -809,7 +794,7 @@ by move=> i; rewrite inE/= => _; apply: (fIF i). Qed. Lemma filter_imply [T : Type] [P : Prop] [f : set T] [F : set_system T] : - Filter F -> (P -> \near F, f F) -> \near F, P -> f F. + Filter F -> (P -> \forall x \near F, f x) -> \forall x \near F, P -> f x. Proof. move=> ? PF; near do move=> /asboolP. by case: asboolP=> [/PF|_]; by [apply: filterS|apply: nearW]. @@ -990,7 +975,7 @@ HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) := Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) : {for x, continuous f} -> - (\forall y \near f x, P y) -> (\near x, P (f x)). + (\forall y \near f x, P y) -> (\forall x0 \near x, P (f x0)). Proof. exact. Qed. Arguments near_fun {T T'} f x. @@ -1223,7 +1208,7 @@ split. - move=> fFAG; split. + exact/(cvg_trans fFAG)/cvg_within. + by apply/fFAG; exact: withinT. -- move=> [+ fA] B => /[apply]; rewrite 2!nbhs_nearE !near_map. +- move=> [+ fA] B => /[apply]; rewrite nbhs_simpl. by apply: filterS2 fA => t ?; exact. Unshelve. all: by end_near. Qed. diff --git a/theories/derive.v b/theories/derive.v index c1394a9295..c99c2c9e08 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -891,7 +891,7 @@ rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT. rewrite -ler_pdivlMl //. suff : `|x| <= k%:num ^-1 * e%:num. by apply: le_trans; rewrite num_le_max /= lexx. -near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm. +near: x; apply/nbhs_le_nbhs_norm. by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW. Unshelve. all: by end_near. Qed. @@ -2197,7 +2197,7 @@ Qed. Lemma near_eq_derive {R : numFieldType} {V W : normedModType R} (f g : V -> W) (a v : V) : - (\near a, f a = g a) -> 'D_v f a = 'D_v g a. + (\forall a0 \near a, f a0 = g a0) -> 'D_v f a = 'D_v g a. Proof. have [-> _|] := eqVneq v 0; first by rewrite !derive0. move=> v0 fg; rewrite /derive; congr (lim _). @@ -2207,7 +2207,7 @@ Unshelve. all: by end_near. Qed. Lemma near_eq_is_derive {R : numFieldType} {V W : normedModType R} (f g : V -> W) (a v : V) (df : W) : - (\near a, f a = g a) -> is_derive a v f df -> is_derive a v g df. + (\forall a0 \near a, f a0 = g a0) -> is_derive a v f df -> is_derive a v g df. Proof. move=> fg [fav <-]; rewrite (near_eq_derive _ fg). by apply: DeriveDef => //; exact: near_eq_derivable fav. @@ -2222,7 +2222,7 @@ Lemma near_eq_derive1n_near n f g x: Proof. move=> fg; elim: n => [//|n IH]. near do (rewrite 2!derive1nS !derive1E; apply: near_eq_derive). -by rewrite near_nbhs; exact: near_join. +exact: (@near_join _ x). Unshelve. all: by end_near. Qed. Lemma near_eq_derive1_near f g x : {near x, f =1 g} -> {near x, f^`() =1 g^`()}. diff --git a/theories/ereal.v b/theories/ereal.v index ccad22dcb5..2988cf8398 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1622,15 +1622,16 @@ Qed. Section nbhs_ereal. Context {R : numFieldType} (P : \bar R -> Prop). -Lemma nbhs_EFin (x : R) : (\forall y \near x%:E, P y) <-> \near x, P x%:E. -Proof. done. Qed. +Lemma nbhs_EFin (x : R) : + (\forall y \near x%:E, P y) <-> \forall x0 \near x, P x0%:E. +Proof. by []. Qed. End nbhs_ereal. Section cvg_fin. Context {R : numFieldType} {F : set_system \bar R} {FF : Filter F}. -Lemma fcvg_is_fine a : F --> a%:E -> \near F, F \is a fin_num. +Lemma fcvg_is_fine a : F --> a%:E -> \forall x \near F, x \is a fin_num. Proof. by apply; apply/nbhs_EFin; near=> x. Unshelve. all: by end_near. Qed. End cvg_fin. @@ -1653,7 +1654,8 @@ Section limit. Context {R : numFieldType} {I : Type} {F : set_system I} {FF : Filter F} (f : I -> \bar R). -Lemma cvg_EFin a : (\near F, f F \is a fin_num) -> fine \o f @ F --> a -> +Lemma cvg_EFin a : + (\forall x \near F, f x \is a fin_num) -> fine \o f @ F --> a -> f @ F --> a%:E. Proof. move=> Ffin Fa P/= /nbhs_EFin /Fa; rewrite !near_simpl. @@ -1663,11 +1665,12 @@ Qed. Lemma fine_cvg a : f @ F --> a%:E -> fine \o f @ F --> a. Proof. exact: fine_fcvg. Qed. -Lemma cvg_is_fine a : f @ F --> a%:E -> \near F, f F \is a fin_num. +Lemma cvg_is_fine a : f @ F --> a%:E -> \forall x \near F, f x \is a fin_num. Proof. exact: fcvg_is_fine. Qed. Lemma fine_cvgP a : - f @ F --> a%:E <-> (\near F, f F \is a fin_num) /\ fine \o f @ F --> a. + f @ F --> a%:E <-> + (\forall x \near F, f x \is a fin_num) /\ fine \o f @ F --> a. Proof. by split;[split;[exact: (@cvg_is_fine a)|exact: fine_cvg]|case; apply: cvg_EFin]. Qed. diff --git a/theories/ftc.v b/theories/ftc.v index 6b4b83a07f..0466bc8f54 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1743,7 +1743,7 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R). apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl/=; near=> z. rewrite derive1E deriveN -?derive1E//. apply: dF. - near: z; rewrite near_nbhs. + near: z. apply: (@open_in_nearW _ _ `]a, +oo[). + exact: interval_open. + by move=> ?; rewrite inE. @@ -1785,9 +1785,7 @@ have mF' : measurable_fun `]a, +oo[ (- F)%R^`(). apply: near_eq_cvg => /=; rewrite near_simpl; near=> z. rewrite !derive1E deriveN ?opprK//. apply: dF. - near: z. - rewrite near_nbhs. - exact: near_in_itvoy. + by near: z; exact: near_in_itvoy. rewrite -!integral_itvob_itvcb. - apply/measurable_EFinP; apply: measurable_funM; last exact: measurableT_comp. apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)). diff --git a/theories/landau.v b/theories/landau.v index e5f42d5f75..c3772a092e 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -1115,7 +1115,8 @@ Lemma linear_for_continuous (f : {linear U -> V | GRing.Scale.Law.sort s}) : (f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f. Proof. move=> /eqO_exP [_/posnumP[k0] Of1] x. -apply/cvgrPdist_lt => _/posnumP[e]; rewrite !near_simpl. +apply/cvgrPdist_lt => /= _/posnumP[e]. +suff: \forall t \near x, `|f x - f t| < e%:num by []. rewrite (near_shift 0) /= subr0; near=> y => /=. rewrite -linearB opprD addrC addrNK linearN normrN; near: y. suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|. diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v index 65f3bed060..105cc2e833 100644 --- a/theories/normedtype_theory/ereal_normedtype.v +++ b/theories/normedtype_theory/ereal_normedtype.v @@ -29,7 +29,6 @@ From mathcomp Require Import topology ereal num_normedtype. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -432,24 +431,26 @@ End ereal_is_hausdorff. Hint Extern 0 (hausdorff_space _) => solve[apply: ereal_hausdorff] : core. Section ProperFilterERealType. -Context {T : Type} {a : set_system T} {Fa : ProperFilter a} {R : realFieldType}. +Context {T : Type} {F : set_system T} {FF : ProperFilter F} {R : realFieldType}. Local Open Scope ereal_scope. Implicit Types f g h : T -> \bar R. -Lemma cvge_to_ge f b c : f @ a --> c -> (\near a, b <= f a) -> b <= c. +Lemma cvge_to_ge f b c : f @ F --> c -> (\forall a \near F, b <= f a) -> b <= c. Proof. by move=> /[swap]/(closed_cvg _ (@closed_ereal_le_ereal _ b)) /[apply]. Qed. -Lemma cvge_to_le f b c : f @ a --> c -> (\near a, f a <= b) -> c <= b. +Lemma cvge_to_le f b c : f @ F --> c -> (\forall a \near F, f a <= b) -> c <= b. Proof. by move=> /[swap]/(closed_cvg _ (@closed_ereal_ge_ereal _ b))/[apply]. Qed. -Lemma lime_ge x f : cvg (f @ a) -> (\near a, x <= f a) -> x <= lim (f @ a). +Lemma lime_ge x f : + cvg (f @ F) -> (\forall a \near F, x <= f a) -> x <= lim (f @ F). Proof. exact: cvge_to_ge. Qed. -Lemma lime_le x f : cvg (f @ a) -> (\near a, x >= f a) -> x >= lim (f @ a). +Lemma lime_le x f : + cvg (f @ F) -> (\forall a \near F, x >= f a) -> x >= lim (f @ F). Proof. exact: cvge_to_le. Qed. End ProperFilterERealType. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 0762549e62..ab0502dba0 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -802,16 +802,18 @@ Section ProperFilterRealType. Context {T : Type} {F : set_system T} {FF : ProperFilter F} {R : realFieldType}. Implicit Types (f g h : T -> R) (a b : R). -Lemma cvgr_to_ge f a b : f @ F --> a -> (\near F, b <= f F) -> b <= a. +Lemma cvgr_to_ge f a b : f @ F --> a -> (\forall x \near F, b <= f x) -> b <= a. Proof. by move=> /[swap]/(closed_cvg _ (@closed_ge _ b))/[apply]. Qed. -Lemma cvgr_to_le f a b : f @ F --> a -> (\near F, f F <= b) -> a <= b. +Lemma cvgr_to_le f a b : f @ F --> a -> (\forall x \near F, f x <= b) -> a <= b. Proof. by move=> /[swap]/(closed_cvg _ (@closed_le _ b))/[apply]. Qed. -Lemma limr_ge x f : cvg (f @ F) -> (\near F, x <= f F) -> x <= lim (f @ F). +Lemma limr_ge x f : cvg (f @ F) -> + (\forall x0 \near F, x <= f x0) -> x <= lim (f @ F). Proof. exact: cvgr_to_ge. Qed. -Lemma limr_le x f : cvg (f @ F) -> (\near F, x >= f F) -> x >= lim (f @ F). +Lemma limr_le x f : cvg (f @ F) -> + (\forall x0 \near F, x >= f x0) -> x >= lim (f @ F). Proof. exact: cvgr_to_le. Qed. End ProperFilterRealType. @@ -1269,7 +1271,7 @@ Proof. by move=> ? fa; rewrite -(cvg_lim _ fa) ?lime_le//=; apply: cvgP fa. Qed. Lemma cvg_nnesum (J : Type) (r : seq J) (f : J -> I -> \bar R) (l : J -> \bar R) (P : pred J) : - (forall j, P j -> \near F, 0 <= f j F) -> + (forall j, P j -> \forall i \near F, 0 <= f j i) -> (forall j, P j -> f j @ F --> l j) -> \sum_(j <- r | P j) f j i @[i --> F] --> \sum_(j <- r | P j) l j. Proof. @@ -1284,7 +1286,7 @@ Qed. Lemma lim_nnesum (J : Type) (r : seq J) (f : J -> I -> \bar R) (l : J -> \bar R) (P : pred J) : - (forall j, P j -> \near F, 0 <= f j F) -> + (forall j, P j -> \forall i \near F, 0 <= f j i) -> (forall j, P j -> cvg (f j @ F)) -> lim (\sum_(j <- r | P j) f j i @[i --> F]) = \sum_(j <- r | P j) (lim (f j @ F)). Proof. by move=> ? ?; apply/cvg_lim => //; apply: cvg_nnesum. Qed. @@ -1292,10 +1294,11 @@ Proof. by move=> ? ?; apply/cvg_lim => //; apply: cvg_nnesum. Qed. End ecvg_realFieldType_proper. Section cvg_0_pinfty. -Context {R : realFieldType} {I : Type} {a : set_system I} {FF : Filter a}. +Context {R : realFieldType} {I : Type} {F : set_system I} {FF : Filter F}. Implicit Types f : I -> R. -Lemma gtr0_cvgV0 f : (\near a, 0 < f a) -> f\^-1 @ a --> 0 <-> f @ a --> +oo. +Lemma gtr0_cvgV0 f : (\forall a \near F, 0 < f a) -> + f\^-1 @ F --> 0 <-> f @ F --> +oo. Proof. move=> f_gt0; split; last first. move=> /cvgryPgt cvg_f_oo; apply/cvgr0Pnorm_lt => _/posnumP[e]. @@ -1307,19 +1310,22 @@ near=> M; near=> i; suff: `|(f i)^-1| < M^-1. by near: i; apply: uB; rewrite ?invr_gt0. Unshelve. all: by end_near. Qed. -Lemma cvgrVy f : (\near a, 0 < f a) -> f\^-1 @ a --> +oo <-> f @ a --> 0. +Lemma cvgrVy f : (\forall a \near F, 0 < f a) -> + f\^-1 @ F --> +oo <-> f @ F --> 0. Proof. by move=> f_gt0; rewrite -gtr0_cvgV0 ?inv_funK//; near do rewrite invr_gt0. Unshelve. all: by end_near. Qed. -Lemma ltr0_cvgV0 f : (\near a, 0 > f a) -> f\^-1 @ a --> 0 <-> f @ a --> -oo. +Lemma ltr0_cvgV0 f : (\forall a \near F, 0 > f a) -> + f\^-1 @ F --> 0 <-> f @ F --> -oo. Proof. move=> fL0; rewrite -cvgNP oppr0 (_ : - f\^-1 = (- f)\^-1). by apply/funeqP => i; rewrite opprfctE/= invrN. by rewrite gtr0_cvgV0 ?cvgNry//; near do rewrite oppr_gt0. Unshelve. all: by end_near. Qed. -Lemma cvgrVNy f : (\near a, 0 > f a) -> f\^-1 @ a --> -oo <-> f @ a --> 0. +Lemma cvgrVNy f : (\forall a \near F, 0 > f a) -> + f\^-1 @ F --> -oo <-> f @ F --> 0. Proof. by move=> f_lt0; rewrite -ltr0_cvgV0 ?inv_funK//; near do rewrite invr_lt0. Unshelve. all: by end_near. Qed. @@ -1327,18 +1333,18 @@ Unshelve. all: by end_near. Qed. End cvg_0_pinfty. Section FilterRealType. -Context {T : Type} {a : set_system T} {Fa : Filter a} {R : realFieldType}. +Context {T : Type} {F : set_system T} {FF : Filter F} {R : realFieldType}. Implicit Types f g h : T -> R. -Lemma ger_cvgy f g : (\near a, f a <= g a) -> - f @ a --> +oo -> g @ a --> +oo. +Lemma ger_cvgy f g : (\forall a \near F, f a <= g a) -> + f @ F --> +oo -> g @ F --> +oo. Proof. move=> uv /cvgryPge ucvg; apply/cvgryPge => A. by near=> x do rewrite (le_trans _ (near uv x _))//. Unshelve. all: end_near. Qed. -Lemma ler_cvgNy f g : (\near a, f a >= g a) -> - f @ a --> -oo -> g @ a --> -oo. +Lemma ler_cvgNy f g : (\forall a \near F, f a >= g a) -> + f @ F --> -oo -> g @ F --> -oo. Proof. move=> uv /cvgrNyPle ucvg; apply/cvgrNyPle => A. by near=> x do rewrite (le_trans (near uv x _))//. @@ -1347,53 +1353,54 @@ Unshelve. all: end_near. Qed. End FilterRealType. Section TopoProperFilterRealType. -Context {T : topologicalType} {a : set_system T} {Fa : ProperFilter a}. +Context {T : topologicalType} {F : set_system T} {Fa : ProperFilter F}. Context {R : realFieldType}. Implicit Types f g h : T -> R. -Lemma ler_cvg_to f g (l l' : R) : f @ a --> l -> g @ a --> l' -> - (\near a, f a <= g a) -> l <= l'. +Lemma ler_cvg_to f g (l l' : R) : f @ F --> l -> g @ F --> l' -> + (\forall a \near F, f a <= g a) -> l <= l'. Proof. move=> fl gl; under eq_near do rewrite -subr_ge0; rewrite -subr_ge0. by apply: cvgr_to_ge; apply: cvgB. Qed. -Lemma ler_lim f g : cvg (f @ a) -> cvg (g @ a) -> - (\near a, f a <= g a) -> lim (f @ a) <= lim (g @ a). +Lemma ler_lim f g : cvg (f @ F) -> cvg (g @ F) -> + (\forall a \near F, f a <= g a) -> lim (f @ F) <= lim (g @ F). Proof. exact: ler_cvg_to. Qed. End TopoProperFilterRealType. Section FilterERealType. -Context {T : Type} {a : set_system T} {Fa : Filter a} {R : realFieldType}. +Context {T : Type} {F : set_system T} {FF : Filter F} {R : realFieldType}. Local Open Scope ereal_scope. Implicit Types f g h : T -> \bar R. -Lemma gee_cvgy f g : (\near a, f a <= g a) -> - f @ a --> +oo -> g @ a --> +oo. +Lemma gee_cvgy f g : (\forall a \near F, f a <= g a) -> + f @ F --> +oo -> g @ F --> +oo. Proof. move=> uv /cvgeyPge uecvg; apply/cvgeyPge => A. by near=> x do rewrite (le_trans _ (near uv x _))//. Unshelve. all: end_near. Qed. -Lemma lee_cvgNy f g : (\near a, f a >= g a) -> - f @ a --> -oo -> g @ a --> -oo. +Lemma lee_cvgNy f g : (\forall a \near F, f a >= g a) -> + f @ F --> -oo -> g @ F --> -oo. Proof. move=> uv /cvgeNyPle uecvg; apply/cvgeNyPle => A. by near=> x do rewrite (le_trans (near uv x _))//. Unshelve. all: end_near. Qed. -Lemma squeeze_fin f g h : (\near a, f a <= g a <= h a) -> - (\near a, f a \is a fin_num) -> (\near a, h a \is a fin_num) -> - (\near a, g a \is a fin_num). +Lemma squeeze_fin f g h : (\forall a \near F, f a <= g a <= h a) -> + (\forall a \near F, f a \is a fin_num) -> + (\forall a \near F, h a \is a fin_num) -> + (\forall a \near F, g a \is a fin_num). Proof. apply: filterS3 => x /andP[fg gh]. rewrite !fin_numElt => /andP[oof _] /andP[_ hoo]. by rewrite (lt_le_trans oof) ?(le_lt_trans gh). Qed. -Lemma squeeze_cvge f g h : (\near a, f a <= g a <= h a) -> - forall l : \bar R, f @ a --> l -> h @ a --> l -> g @ a --> l. +Lemma squeeze_cvge f g h : (\forall a \near F, f a <= g a <= h a) -> + forall l : \bar R, f @ F --> l -> h @ F --> l -> g @ F --> l. Proof. move=> fgh [l||]; last 2 first. - by move=> + _; apply: gee_cvgy; apply: filterS fgh => ? /andP[]. @@ -1405,17 +1412,17 @@ by have /(_ _)/andP[//|fg gh] := near fgh x; rewrite !fine_le//=; near: x. Unshelve. all: end_near. Qed. End FilterERealType. -Arguments squeeze_fin {T a Fa R} f g h. -Arguments squeeze_cvge {T a Fa R} f g h. +Arguments squeeze_fin {T F FF R} f g h. +Arguments squeeze_cvge {T F FF R} f g h. Section TopoProperFilterERealType. -Context {T : topologicalType} {a : set_system T} {Fa : ProperFilter a}. -Context {R : realFieldType}. +Context {T : topologicalType} {F : set_system T} {FF : ProperFilter F} + {R : realFieldType}. Local Open Scope ereal_scope. Implicit Types f g h : T -> \bar R. -Lemma lee_cvg_to f g l l' : f @ a --> l -> g @ a --> l' -> - (\near a, f a <= g a) -> l <= l'. +Lemma lee_cvg_to f g l l' : f @ F --> l -> g @ F --> l' -> + (\forall a \near F, f a <= g a) -> l <= l'. Proof. move=> + + fg; move: l' l. move=> /= [l'||] [l||]//=; rewrite ?leNye ?leey//=; first 1 last. @@ -1427,14 +1434,14 @@ rewrite lee_fin -(cvg_lim _ fl)// -(cvg_lim _ gl)//. by apply: ler_lim; [apply: cvgP fl|apply: cvgP gl|near do apply: fine_le]. Unshelve. all: end_near. Qed. -Lemma lee_lim f g : cvg (f @ a) -> cvg (g @ a) -> - (\near a, f a <= g a) -> lim (f @ a) <= lim (g @ a). +Lemma lee_lim f g : cvg (f @ F) -> cvg (g @ F) -> + (\forall a \near F, f a <= g a) -> lim (f @ F) <= lim (g @ F). Proof. exact: lee_cvg_to. Qed. End TopoProperFilterERealType. Section Rhull. -Variable R : realType. +Context {R : realType}. Definition Rhull (X : set R) : interval R := Interval (if `[< has_lbound X >] then BSide `[< X (inf X) >] (inf X) diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index fd1f48c89b..ea6cadd6df 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -1019,11 +1019,11 @@ Let near_at_left (a : itv_bound R) b f eps : (a < BLeft b)%O -> 0 < eps -> Proof. move=> ab eps_gt0 cf. move/continuous_withinNx/cvg_ballP/(_ _ eps_gt0) : (cf b). -rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=. +rewrite /dnbhs/= near_withinE /prop_near1 /nbhs/=. rewrite -nbhs_subspace_in//. rewrite /= in_itv/= lexx andbT. by move: a ab {cf} => [[a|a]/=|[|]//]; rewrite bnd_simp// => /ltW. -rewrite /within/= near_simpl; apply: filter_app. +rewrite /within/=; apply: filter_app. move: a ab {cf} => [a0 a/= /[!bnd_simp] ab|[_|//]]. - exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=. @@ -1038,11 +1038,11 @@ Let near_at_right a (b : itv_bound R) f eps : (BRight a < b)%O -> 0 < eps -> Proof. move=> ab eps_gt0 cf. move/continuous_withinNx/cvg_ballP/(_ _ eps_gt0) : (cf a). -rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=. +rewrite /dnbhs/= near_withinE /prop_near1 /nbhs/=. rewrite -nbhs_subspace_in//. rewrite /= in_itv/= lexx//=. by move: b ab {cf} => [[b|b]/=|[|]//]; rewrite bnd_simp// => /ltW. -rewrite /within/= near_simpl; apply: filter_app. +rewrite /within/=; apply: filter_app. move: b ab {cf} => [b0 b/= /[!bnd_simp] ab|[//|_]]. - exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=. @@ -1071,10 +1071,12 @@ apply/subspace_continuousP => x /=. rewrite in_itv/= => /andP[ax xb]. move: ctsL ctsR. have : a = x /\ ba \/ a < x. - clear - ax. case: ba ax => /=; last by right. + clear - ax. + case: ba ax => /=; last by right. by case: ltgtP => //; [right|left]. have : b = x /\ (bb = false) \/ x < b. - clear - xb. case: bb xb => /=; first by right. + clear - xb. + case: bb xb => /=; first by right. by case: ltgtP => //; [right|left]. move=> {ax xb}. move=> [[<- ->]|xb] [[+ ->]|ax]. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index eb070aab1b..c1256106cb 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -594,7 +594,8 @@ which causes an inference problem in derive.v *) Lemma nbhs_nbhs_norm : nbhs_norm = nbhs. Proof. by rewrite ball_normE funeqE => x; rewrite -filter_from_ballE. Qed. -Lemma nbhs_normP x (P : V -> Prop) : (\near x, P x) <-> nbhs_norm x P. +Lemma nbhs_normP x (P : V -> Prop) : + (\forall x0 \near x, P x0) <-> nbhs_norm x P. Proof. by rewrite nbhs_nbhs_norm. Qed. Lemma nbhs_le_nbhs_norm (x : V) : @nbhs V _ x `=>` nbhs_norm x. @@ -608,23 +609,22 @@ Lemma filter_from_norm_nbhs x : Proof. by rewrite -nbhs_nbhs_norm ball_normE. Qed. Lemma nbhs_normE (x : V) (P : V -> Prop) : - nbhs_norm x P = \near x, P x. + nbhs_norm x P = \forall x0 \near x, P x0. Proof. by rewrite nbhs_nbhs_norm near_simpl. Qed. Lemma filter_from_normE (x : V) (P : V -> Prop) : - @filter_from K _ [set x : K | 0 < x] (ball_norm x) P = \near x, P x. + @filter_from K _ [set x : K | 0 < x] (ball_norm x) P = \forall x0 \near x, P x0. Proof. by rewrite filter_from_norm_nbhs. Qed. Lemma near_nbhs_norm (x : V) (P : V -> Prop) : - (\forall x \near nbhs_norm x, P x) = \near x, P x. + (\forall x \near nbhs_norm x, P x) = \forall x0 \near x, P x0. Proof. exact: nbhs_normE. Qed. -Lemma nbhs_norm_ball_norm x (e : {posnum K}) : - nbhs_norm x (ball_norm x e%:num). +Lemma nbhs_norm_ball_norm x (e : {posnum K}) : nbhs_norm x (ball_norm x e%:num). Proof. by rewrite ball_normE; exists e%:num => /=. Qed. Lemma nbhs_ball_norm (x : V) (eps : {posnum K}) : nbhs x (ball_norm x eps%:num). -Proof. rewrite -nbhs_nbhs_norm; apply: nbhs_norm_ball_norm. Qed. +Proof. by rewrite -nbhs_nbhs_norm; exact: nbhs_norm_ball_norm. Qed. Lemma ball_norm_dec x y (e : K) : {ball_norm x e y} + {~ ball_norm x e y}. Proof. exact: pselect. Qed. @@ -712,7 +712,7 @@ Lemma nbhs_norm_ball x (eps : {posnum K}) : nbhs_norm x (ball x eps%:num). Proof. by rewrite nbhs_nbhs_norm; exact: nbhsx_ballx. Qed. Lemma nbhsDl (P : set V) (x y : V) : - (\forall z \near (x + y), P z) <-> (\near x, P (x + y)). + (\forall z \near (x + y), P z) <-> (\forall x0 \near x, P (x0 + y)). Proof. split=> /nbhs_normP[_/posnumP[e]/= Px]; apply/nbhs_normP; exists e%:num => //=. by move=> z /= xze; apply: Px; rewrite /= [z + y]addrC addrKA. @@ -720,14 +720,15 @@ by move=> z /= xyz; rewrite -[z](addrNK y); apply: Px; rewrite /= opprB addrA. Qed. Lemma nbhsDr (P : set V) x y : - (\forall z \near (x + y), P z) <-> (\near y, P (x + y)). + (\forall z \near (x + y), P z) <-> (\forall y0 \near y, P (x + y0)). Proof. by rewrite addrC nbhsDl -propeqE; apply: eq_near => ?; rewrite addrC. Qed. -Lemma nbhs0P (P : set V) x : (\near x, P x) <-> (\forall e \near 0, P (x + e)). +Lemma nbhs0P (P : set V) x : + (\forall x0 \near x, P x0) <-> (\forall e \near 0, P (x + e)). Proof. by rewrite -nbhsDr addr0. Qed. Lemma near_shift (y x : V) (P : set V) : - (\near x, P x) = (\forall z \near y, (P \o shift (x - y)) z). + (\forall x0 \near x, P x0) = (\forall z \near y, (P \o shift (x - y)) z). Proof. rewrite propeqE nbhs0P [X in _ <-> X]nbhs0P/= -propeqE. by apply: eq_near => e; rewrite [_ + _ + _]addrC subrKA. @@ -1067,15 +1068,17 @@ Context {R : numFieldType}. Lemma nbhs_right0P x (P : set R) : (\forall y \near x^'+, P y) <-> \forall e \near 0^'+, P (x + e). Proof. -rewrite !near_withinE !near_simpl. -rewrite (@nbhs0P R R^o)// -propeqE. +rewrite !near_withinE -[X in X <-> _]nearE [X in X <-> _](@nbhs0P R R^o)//. +rewrite -propeqE. by apply: (@eq_near _ (nbhs (0 : R))) => y; rewrite ltrDl. Qed. Lemma nbhs_left0P x (P : set R) : (\forall y \near x^'-, P y) <-> \forall e \near 0^'+, P (x - e). Proof. -rewrite !near_withinE !near_simpl (@nbhs0P R R^o); split=> Px. +rewrite !near_withinE -[X in X <-> _]nearE -[X in _ <-> X]nearE. +rewrite [X in X <-> _](@nbhs0P R R^o); split=> Px. + suff: \forall x0 \near (0:R), 0 < x0 -> P (x - x0) by []. rewrite -oppr0 nearN; near=> e; rewrite ltrN2 opprK => e_lt0. by apply: (near Px) => //; rewrite gtrDl. by rewrite -oppr0 nearN; near=> e; rewrite gtrDl oppr_lt0; apply: (near Px). @@ -1173,7 +1176,7 @@ Lemma nbhsr0P (P : set V) x : (\forall y \near x, P y) <-> (\forall e \near 0^'+, forall y, `|x - y| <= e -> P y). Proof. -rewrite nbhs0P/= near_withinE/= !near_simpl. +rewrite nbhs0P/= near_withinE/=. split. move => /nbhs_norm0P[/= _/posnumP[e] /(_ _) Px]. apply/(@nbhs_norm0P R R^o). @@ -1432,7 +1435,8 @@ Section realFieldType. Context {R : realFieldType}. Lemma at_right_in_segment (x : R) (P : set R) : - (\forall e \near 0^'+, {in `[x - e, x + e], forall x, P x}) <-> (\near x, P x). + (\forall e \near 0^'+, {in `[x - e, x + e], forall x, P x}) <-> + (\forall x0 \near x, P x0). Proof. rewrite (@nbhsr0P _ R^o) -propeqE; apply: eq_near => y /=. by rewrite -propeqE; apply: eq_forall => z; rewrite ler_distlC. diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v index e8b8cffe4c..65b3893de1 100644 --- a/theories/topology_theory/compact.v +++ b/theories/topology_theory/compact.v @@ -34,7 +34,6 @@ From mathcomp Require Import uniform_structure pseudometric_structure. Import Order.TTheory GRing.Theory Num.Theory. -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -148,7 +147,7 @@ Definition near_covering (K : set X) := forall (I : Type) (F : set_system I) (P : I -> X -> Prop), Filter F -> (forall x, K x -> \forall x' \near x & i \near F, P i x') -> - \near F, K `<=` P F. + \forall i \near F, K `<=` P i. Let near_covering_compact : near_covering `<=` compact. Proof. @@ -199,7 +198,7 @@ Definition near_covering_within (K : set X) := forall (I : Type) (F : set_system I) (P : I -> X -> Prop), Filter F -> (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> - \near F, K `<=` P F. + \forall i \near F, K `<=` P i. Lemma near_covering_withinP (K : set X) : near_covering_within K <-> near_covering K. diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index a1c6577f90..06f4b1a94e 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -241,7 +241,8 @@ rewrite -filter_from_ballE. by rewrite -ball_mdistE. Qed. -Lemma nbhs_mdistP x (P : V -> Prop) : (\near x, P x) <-> nbhs_mdist x P. +Lemma nbhs_mdistP x (P : V -> Prop) : + (\forall x0 \near x, P x0) <-> nbhs_mdist x P. Proof. by rewrite nbhs_nbhs_mdist. Qed. Lemma filter_from_mdist_nbhs (y : V) : @@ -288,7 +289,7 @@ Lemma nbhsr0P (P : set V) x : (\forall y \near x, P y) <-> (\forall e \near 0^'+, forall y, mdist x y <= e -> P y). Proof. -rewrite (*nbhs0P*)/= near_withinE !near_simpl. +rewrite near_withinE. split. move => /nbhs_mdistP[/= _/posnumP[e] /(_ _) Px]. apply/(@nbhs_mdistP R R^o). @@ -414,7 +415,7 @@ Proof. by move=> /cvgr_gt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW. Qed. -Lemma squeeze_cvgr f g h : (\near F, f F <= g F <= h F) -> +Lemma squeeze_cvgr f g h : (\forall x \near F, f x <= g x <= h x) -> forall l : R, f @ F --> l -> h @ F --> l -> g @ F --> l. Proof. move=> fgh l lfa lga. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index d69267d4c4..c219d00f9f 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -20,7 +20,6 @@ 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 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -174,7 +173,7 @@ 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). + (\forall y \near - x, P y) <-> \forall x0 \near x, P (- x0). Proof. by rewrite -[X in X <-> _]near_simpl nbhsN. Qed. Lemma nbhsNimage {R : numFieldType} (x : R) : @@ -381,7 +380,7 @@ Lemma cvg_at_right_left_dnbhs (R : realFieldType) (T : topologicalType) 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. +rewrite !near_withinE => lf rf. apply: filter_app lf; apply: filter_app rf. by near=> t => xlt xgt /lt_total/orP[|]. Unshelve. all: by end_near. Qed. diff --git a/theories/topology_theory/one_point_compactification.v b/theories/topology_theory/one_point_compactification.v index d4b1f70230..f6cd875af6 100644 --- a/theories/topology_theory/one_point_compactification.v +++ b/theories/topology_theory/one_point_compactification.v @@ -15,8 +15,6 @@ From mathcomp Require Import pseudometric_structure compact initial_topology. (* as an alias of `option X` *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) - Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -70,7 +68,7 @@ Lemma one_point_compactification_compact : compact [set: opc]. Proof. apply/compact_near_coveringP => ? F /= P FF FT. have [[U i] [[W [cptW cW] /= WU nFi UiP]]] := FT None I. -have P'F x : W x -> \near x & F, P F (Some x). +have P'F x : W x -> \forall x0 \near x & x1 \near F, P x1 (Some x0). move=> Wx; suff: \forall y \near Some @ x & f \near id @ F, P f y. by rewrite near_map2. exact: FT (Some x) I. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index 4248631002..9f51b893a4 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -312,7 +312,7 @@ Lemma cvg_withinP {T : topologicalType} {R : archiRealFieldType} Proof. split=> [fpl u [Au up]|ful]. move=> V Vnb. - have := fpl _ Vnb; rewrite {1 2 4}/nbhs/= /within/= near_nbhs => Unb. + have := fpl _ Vnb; rewrite {1 2 4}/nbhs/= /within/= => Unb. have [N _ {}up] := up _ Unb. by exists N => // n /= Nn; exact: up. apply: contrapT => fpl; move: ful; apply/existsNP. @@ -326,7 +326,7 @@ have [V Vnb hV] : exists2 V : set T, nbhs l V & forall d : {posnum R}, rewrite nbhs_nearE near_map near_withinE; near=> t => At. have /not_and3P[//|bp|/contrapT //] := h t. exfalso; apply: bp. - by rewrite ball_symE; near: t; rewrite !near_nbhs; apply: near_ball. + by rewrite ball_symE; near: t; apply: near_ball. have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0. exists (fun n => sval (cid (hV (PosNum (invn n))))). - split => [k|]; first by rewrite /sval/=; case: cid => x []. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index e1607edf91..f09196aadd 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -282,7 +282,7 @@ Qed. End Topological1. Lemma open_in_nearW {T : topologicalType} (P : T -> Prop) (S : set T) : - open S -> {in S, forall x, P x} -> {in S, forall x, \near x, P x}. + open S -> {in S, forall x, P x} -> {in S, forall x, \forall x0 \near x, P x0}. Proof. by move=> oS SP z /set_mem Sz; apply: in_nearW SP => //=; exact: open_nbhs_nbhs. Qed. @@ -313,27 +313,29 @@ move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA]. by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA]. Qed. -Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) : +Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) : {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D). Proof. rewrite !openE => fcont Dop x /= Dfx. by apply: fcont; [rewrite inE|exact: Dop]. Qed. -Lemma cvg_fmap {T: topologicalType} {U : topologicalType} +Lemma cvg_fmap {T : topologicalType} {U : topologicalType} (F : set_system T) x (f : T -> U) : {for x, continuous f} -> F --> x -> f @ F --> f x. Proof. by move=> cf fx P /cf /fx. Qed. Lemma near_join (T : topologicalType) (x : T) (P : set T) : - (\near x, P x) -> \near x, \near x, P x. + (\forall x0 \near x, P x0) -> \forall x0 \near x, \forall x1 \near x0, P x1. Proof. exact: nbhs_interior. Qed. Lemma near_bind (T : topologicalType) (P Q : set T) (x : T) : - (\near x, (\near x, P x) -> Q x) -> (\near x, P x) -> \near x, Q x. + (\forall x0 \near x, (\forall x1 \near x, P x1) -> Q x0) -> + (\forall x0 \near x, P x0) -> + \forall x0 \near x, Q x0. Proof. move=> PQ xP; near=> y; apply: (near PQ y) => //; -by apply: (near (near_join xP) y). +exact: (near (near_join xP) y). Unshelve. all: by end_near. Qed. (* limit composition *) @@ -831,10 +833,10 @@ Lemma closedT : closed setT. Proof. by []. Qed. Lemma closed0 : closed set0. Proof. by move=> ? /(_ setT) [|? []] //; apply: filterT. Qed. -Lemma closedE : closed = [set A : set T | forall p, ~ (\near p, ~ A p) -> A p]. +Lemma closedE : closed = [set A : set T | forall p, ~ (\forall x \near p, ~ A x) -> A p]. Proof. rewrite predeqE => A; split=> Acl p; last first. - by move=> clAp; apply: Acl; rewrite -nbhs_nearE => /clAp [? []]. + by move=> clAp; apply: Acl => /clAp [? []]. rewrite -nbhs_nearE nbhsE => /asboolP. rewrite asbool_neg => /forallp_asboolPn2 clAp. apply: Acl => B; rewrite nbhsE => - [C [oC pC]]. @@ -845,10 +847,7 @@ by exists q. Qed. Lemma closed_openC (D : set T) : closed D -> open (~` D). -Proof. -rewrite closedE openE => Dcl t nDt; apply: contrapT. -by rewrite /interior nbhs_nearE => /Dcl. -Qed. +Proof. by rewrite closedE openE => Dcl t nDt; apply: contrapT => /Dcl. Qed. Lemma closedC (D : set T) : closed (~` D) = open D. Proof. @@ -871,7 +870,7 @@ Proof. rewrite !closedE=> f_continuous D_cl x /= xDf. apply: D_cl; apply: contra_not xDf => fxD. have NDfx : ~ D (f x). - by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; exact. + move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; exact. by apply: f_continuous fxD; rewrite inE. Qed. #[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `preimage_closed`")] diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index f4945b2033..ce77dcc5ea 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.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"] @@ -44,7 +44,6 @@ From mathcomp Require Import topology_structure. (* ``` *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -281,7 +280,7 @@ Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x : Proof. split=> - cfx P /= fxP. by rewrite !near_simpl; apply: cvg_within; apply: cfx. -rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP. +rewrite !nbhs_nearE !near_map in fxP *; have /= := cfx P fxP. rewrite !near_simpl near_withinE near_simpl => Pf; near=> y. by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. Unshelve. all: by end_near. Qed. From cbda6a08078b5283f0ea1d634a302dbe9fb41276 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 26 Oct 2026 19:41:47 +0900 Subject: [PATCH 2/3] restore near_nbhs and fix back near_simpl --- CHANGELOG_UNRELEASED.md | 1 - classical/filter.v | 6 +++++- theories/normedtype_theory/pseudometric_normed_Zmodule.v | 4 ++-- theories/topology_theory/topology_structure.v | 4 ++-- 4 files changed, 9 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c125ad66d6..67aa2ec070 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -389,7 +389,6 @@ - in `filter.v`: + notation `\near x, P x` + notation `\near x & y, P x y` - + lemma `near_nbhs` ### Infrastructure diff --git a/classical/filter.v b/classical/filter.v index 878c6897df..83acb96121 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -394,6 +394,10 @@ Lemma nbhs_nearE {U} {T : filteredType U} (x : T) (P : set U) : nbhs x P = \forall x0 \near x, P x0. Proof. by []. Qed. +Lemma near_nbhs {U} {T : filteredType U} (x : T) (P : set U) : + (\forall x0 \near nbhs x, P x0) = (\forall x0 \near x, P x0). +Proof. by []. Qed. + Lemma near2_curry {U V} (F : set_system U) (G : set_system V) (P : U -> set V) : {near F & G, forall x y, P x y} = {near (F, G), forall x, P x.1 x.2}. Proof. by []. Qed. @@ -410,7 +414,7 @@ Lemma filter_of_nearI (X : Type) (fX : filteredType X) Proof. by []. Qed. Module Export NearNbhs. -Definition near_simpl := (filter_of_nearI). +Definition near_simpl := (@near_nbhs, filter_of_nearI). Ltac near_simpl := rewrite ?near_simpl. End NearNbhs. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index c1256106cb..b0c52ff23e 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1068,7 +1068,7 @@ Context {R : numFieldType}. Lemma nbhs_right0P x (P : set R) : (\forall y \near x^'+, P y) <-> \forall e \near 0^'+, P (x + e). Proof. -rewrite !near_withinE -[X in X <-> _]nearE [X in X <-> _](@nbhs0P R R^o)//. +rewrite !near_withinE -[X in X <-> _]nearE !near_simpl (@nbhs0P _ R^o). rewrite -propeqE. by apply: (@eq_near _ (nbhs (0 : R))) => y; rewrite ltrDl. Qed. @@ -1077,7 +1077,7 @@ Lemma nbhs_left0P x (P : set R) : (\forall y \near x^'-, P y) <-> \forall e \near 0^'+, P (x - e). Proof. rewrite !near_withinE -[X in X <-> _]nearE -[X in _ <-> X]nearE. -rewrite [X in X <-> _](@nbhs0P R R^o); split=> Px. +rewrite !near_simpl (@nbhs0P R R^o); split=> Px. suff: \forall x0 \near (0:R), 0 < x0 -> P (x - x0) by []. rewrite -oppr0 nearN; near=> e; rewrite ltrN2 opprK => e_lt0. by apply: (near Px) => //; rewrite gtrDl. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index f09196aadd..2a30f0e29a 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -867,10 +867,10 @@ Notation closure_limit_point := __deprecated__closure_limit_point (only parsing) Lemma preimage_closed {T U : topologicalType} (f : T -> U) (D : set U) : {in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D). Proof. -rewrite !closedE=> f_continuous D_cl x /= xDf. +rewrite !closedE => f_continuous D_cl x /= xDf. apply: D_cl; apply: contra_not xDf => fxD. have NDfx : ~ D (f x). - move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; exact. + by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; exact. by apply: f_continuous fxD; rewrite inE. Qed. #[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `preimage_closed`")] From 32fbd2337264d8272899d28c5949af23fac33dce Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 26 Oct 2026 19:48:00 +0900 Subject: [PATCH 3/3] rm unused ltac --- CHANGELOG_UNRELEASED.md | 1 + classical/filter.v | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67aa2ec070..bae2e2e58f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -389,6 +389,7 @@ - in `filter.v`: + notation `\near x, P x` + notation `\near x & y, P x y` + + ltac `near_simpl` ### Infrastructure diff --git a/classical/filter.v b/classical/filter.v index 83acb96121..591459b297 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -415,7 +415,6 @@ Proof. by []. Qed. Module Export NearNbhs. Definition near_simpl := (@near_nbhs, filter_of_nearI). -Ltac near_simpl := rewrite ?near_simpl. End NearNbhs. Lemma near_swap {U V} (F : set_system U) (G : set_system V) (P : U -> set V) :