From 43b6286009ffae90d51810c89813cbc377b84543 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Tue, 24 Feb 2026 14:29:24 +0900 Subject: [PATCH 1/3] rename closure_subset -> closureS; add interiorS --- CHANGELOG_UNRELEASED.md | 16 ++++++++++++---- theories/cantor.v | 2 +- theories/function_spaces.v | 2 +- .../pseudometric_normed_Zmodule.v | 2 +- theories/normedtype_theory/urysohn.v | 10 +++++----- theories/topology_theory/compact.v | 2 +- theories/topology_theory/connected.v | 4 ++-- theories/topology_theory/separation_axioms.v | 4 ++-- theories/topology_theory/subspace_topology.v | 4 ++-- theories/topology_theory/topology_structure.v | 11 +++++++++-- 10 files changed, 36 insertions(+), 21 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 169654f68..0a799011a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,10 +3,15 @@ ## [Unreleased] ### Added -- in order_topology.v +- in `topology_structure.v` + + lemma `interiorS` + +- in `order_topology.v` + lemma `itv_closed_ends_closed` +- in `classical_sets.v` + + lemma `in_set1_eq` -- in set_interval.v +- in `set_interval.v` + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends` - in `Rstruct.v`: @@ -46,10 +51,10 @@ `emeasurable_fun_itv_cc` ### Changed -- in set_interval.v +- in `set_interval.v` + `itv_is_closed_unbounded` (fix the definition) -- in set_interval.v +- in `set_interval.v` + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool) - in `lebesgue_Rintegrable.v`: @@ -168,6 +173,9 @@ ### Renamed +- in `topology_structure.v` + + `closure_subset` -> `closureS` + - in `set_interval.v`: + `itv_is_ray` -> `itv_is_open_unbounded` + `itv_is_bd_open` -> `itv_is_oo` diff --git a/theories/cantor.v b/theories/cantor.v index 880331028..26287d1bc 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -420,7 +420,7 @@ move=> _; split=> [|A [|]| | |]. - move=> [z M'z] <-; exists z; split. + apply: subset_closure; apply: nbhs_singleton; apply: nbhs_interior. by rewrite -nbhs_entourageE; exists (split_ent E) => // t /xsectionP. - + by apply: closure_subset; exact: interior_subset. + + by apply: closureS; exact: interior_subset. - by case => ->; [exists t0 | exists t1]; split => // t ->; apply/subset_closure/xsectionP; exact: entourage_refl. - exists [set t0], [set t1]; split;[|split]. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 9505da948..2c0f8294e 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1245,7 +1245,7 @@ have : compact (proj x @` (closure W)). exact: (@pointwise_cvg_compact_family _ _ (nbhs g)). move=> /[dup]/(compact_closed hsdf)/closure_id -> /subclosed_compact. apply; first exact: closed_closure. -by apply/closure_subset/image_subset; exact: (@subset_closure _ W). +by apply/closureS/image_subset; exact: (@subset_closure _ W). Qed. Lemma pointwise_cvg_entourage (x : X) (f : {ptws X -> Y}) E : diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index bb5d5bdfc..4f37fc0f8 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1199,7 +1199,7 @@ Qed. Lemma le_closed_ball (R : numFieldType) (M : pseudoMetricType R) (x : M) (e1 e2 : R) : (e1 <= e2)%O -> closed_ball x e1 `<=` closed_ball x e2. -Proof. by rewrite /closed_ball => le; apply/closure_subset/le_ball. Qed. +Proof. by rewrite /closed_ball => le; apply/closureS/le_ball. Qed. End Closed_Ball. #[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `closure_ballE`")] diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index d184bd357..94f099d4f 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -472,7 +472,7 @@ have [R' []] : exists R', [/\ open R', closure L `<=` R' & closure R' `<=` R]. have := @normalT (closure L) (@closed_closure T L). case/(_ R); first by move=> x /cLR ?; apply: open_nbhs_nbhs. move=> V /set_nbhsP [U] [? ? ? cVR]; exists U; split => //. - by apply: (subset_trans _ cVR); exact: closure_subset. + by apply: (subset_trans _ cVR); exact: closureS. move=> oR' cLR' cR'R; exists (apxU (L, R')), (apxU (R', R)). split; first by exists (L, R'). exists (R', R) => //; split => //; apply: (subset_trans AL). @@ -556,7 +556,7 @@ move=> V /set_nbhsP [U [oU AU UV]] cVcb. exists (Uniform.class urysohnType), (apxU (U, ~` B)); split => //. - move=> ?; apply:sub_gen_smallest; exists (U, ~`B) => //; split => //=. exact/closed_openC. - by move: UV => /closure_subset/subset_trans; apply. + by move: UV => /closureS/subset_trans; apply. - rewrite eqEsubset; split; case=> // a b [/=[Aa Bb] [[//]|]]. by have /subset_closure ? := AU _ Aa; case. move=> x ? [E gE] /(@filterS T); apply; move: gE. @@ -634,10 +634,10 @@ case/(_ _ _ clA (open_closedC oC) AC0) => U [V] [oU oV AU nCV UV0]. exists (~` closure V). apply/set_nbhsP; exists U; split => //. apply/subsetCr; have := open_closedC oU; rewrite closure_id => ->. - by apply/closure_subset/disjoints_subset; rewrite setIC. + by apply/closureS/disjoints_subset; rewrite setIC. apply/(subset_trans _ CB)/subsetCP; apply: (subset_trans nCV). apply/subsetCr; have := open_closedC oV; rewrite closure_id => ->. -exact/closure_subset/subsetC/subset_closure. +exact/closureS/subsetC/subset_closure. Qed. Lemma normal_openP : normal_space T <-> @@ -820,7 +820,7 @@ move=> + A Ax => /(_ (~` A°)) []; [|exact|]. exact/open_closedC/open_interior. move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U. exact/open_nbhs_nbhs. -apply: (subset_trans (closure_subset UV)). +apply: (subset_trans (closureS UV)). move/open_closedC/closure_id : oV => <-. by apply: (subset_trans cAV); rewrite setCK; exact: interior_subset. Qed. diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v index f72a436b3..58d898e93 100644 --- a/theories/topology_theory/compact.v +++ b/theories/topology_theory/compact.v @@ -261,7 +261,7 @@ rewrite propeqE; split=> [[B CsubB [cptB cB]]|]; last first. move=> clC; exists (closure C) => //; first exact: subset_closure. by split => //; exact: closed_closure. apply: (subclosed_compact _ cptB); first exact: closed_closure. -by move/closure_id: cB => ->; exact: closure_subset. +by move/closure_id: cB => ->; exact: closureS. Qed. Lemma precompact_subset (A B : set X) : diff --git a/theories/topology_theory/connected.v b/theories/topology_theory/connected.v index c5550e92c..20c62edd0 100644 --- a/theories/topology_theory/connected.v +++ b/theories/topology_theory/connected.v @@ -146,7 +146,7 @@ Lemma connected_closure A : connected A -> connected (closure A). Proof. move=> ctdA U U0 [C1 oC1 C1E] [C2 cC2 C2E]; rewrite eqEsubset C2E; split => //. suff : A `<=` U. - move/closure_subset; rewrite [_ `&` _](iffLR (closure_id _)) ?C2E//. + move/closureS; rewrite [_ `&` _](iffLR (closure_id _)) ?C2E//. by apply: closedI => //; exact: closed_closure. rewrite -setIidPl; apply: ctdA. - move: U0; rewrite C1E => -[z [clAx C1z]]; have [] := clAx C1. @@ -217,7 +217,7 @@ rewrite closure_id eqEsubset; split; first exact: subset_closure. move=> z Axz; exists (closure (connected_component A x)) => //. split; first exact/subset_closure/connected_component_refl. rewrite [X in _ `<=` X](closure_id A).1//. - by apply: closure_subset; exact: connected_component_sub. + by apply: closureS; exact: connected_component_sub. by apply: connected_closure; exact: component_connected. Qed. diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 0fb7543b0..e54a5b255 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -477,7 +477,7 @@ split; first by exists A => //; exact: open_nbhs_nbhs. apply/not_implyP; split; first exact: open_nbhs_nbhs. apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset. have /closure_id -> : closed (~` B); first by exact: open_closedC. -by apply/closure_subset/disjoints_subset; rewrite setIC. +by apply/closureS/disjoints_subset; rewrite setIC. Qed. Lemma compact_normal_local (K : set T) : hausdorff_space T -> compact K -> @@ -516,7 +516,7 @@ case/(_ _ _ _ _ cvP) : cvA => R /= [RA Rmono [U RU] RBx]. have [V /set_nbhsP [W [oW cBW WV] clVU]] := RA _ RU; exists (~` W). apply/set_nbhsP; exists (~` closure W); split. - exact/closed_openC/closed_closure. - - by move=> y /(RBx _ RU) + Wy; apply; exact/clVU/(closure_subset WV). + - by move=> y /(RBx _ RU) + Wy; apply; exact/clVU/(closureS WV). - by apply: subsetC; exact/subset_closure. have : closed (~` W) by exact: open_closedC. by rewrite closure_id => <-; exact: subsetCl. diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index d84fb0375..5e65d45d0 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -257,7 +257,7 @@ Lemma closure_subspaceW (U : set T) : U `<=` A -> closure (U : set (subspace A)) = closure (U : set T) `&` A. Proof. have /closed_subspaceP := (@closed_closure _ (U : set (subspace A))). -move=> [V] [clV VAclUA] /[dup] /(@closure_subset (subspace _)). +move=> [V] [clV VAclUA] /[dup] /(@closureS (subspace _)). have /closure_id <- := closed_subspaceT => /setIidr <-; rewrite setIC. move=> UsubA; rewrite eqEsubset; split. apply: setSI; rewrite closureE; apply: smallest_sub (@subset_closure _ U). @@ -628,7 +628,7 @@ have ? : f @` closure (AfE b) `<=` closure (E b). have /(@image_subset _ _ f) : closure (AfE b) `<=` f @^-1` closure (E b). have /closure_id -> : closed (f @^-1` closure (E b) : set (subspace A)). by apply: preimage_closed => //; exact: closed_closure. - apply: closure_subset. + apply: closureS. have /(@preimage_subset _ _ f) A0cA0 := @subset_closure _ (E b). by apply: subset_trans A0cA0; apply: subIset; right. by move/subset_trans; apply; exact: image_preimage_subset. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index faab410d9..78889179c 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -840,12 +840,12 @@ Section closure_lemmas. Variable T : topologicalType. Implicit Types E A B U : set T. -Lemma closure_subset A B : A `<=` B -> closure A `<=` closure B. +Lemma closureS A B : A `<=` B -> closure A `<=` closure B. Proof. by move=> ? ? CAx ?; move/CAx; exact/subsetI_neq0. Qed. Lemma closureE A : closure A = smallest closed A. Proof. -rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closure_subset AB). +rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closureS AB). exact: (smallest_sub (@closed_closure _ _) (@subset_closure _ _)). Qed. @@ -886,6 +886,13 @@ Qed. Lemma closure_setC A : closure (~` A) = ~` A°. Proof. by apply: setC_inj; rewrite -interiorC !setCK. Qed. +Lemma interiorS A B : A `<=` B -> A° `<=` B°. +Proof. +move=> AB x. +rewrite /interior nbhsE => -[] U oxU UA. +exists U => //; move: UA AB; exact: subset_trans. +Qed. + Lemma interior_id A : open A <-> interior A = A. Proof. by rewrite -(setCK A) openC interiorC closure_id; split => [ <- | /setC_inj->]. From 49a006440e4512db258c063fa83ab08f503b3d9c Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Tue, 24 Feb 2026 20:37:47 +0900 Subject: [PATCH 2/3] add deprecation --- theories/topology_theory/topology_structure.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 78889179c..97e66c029 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -843,6 +843,9 @@ Implicit Types E A B U : set T. Lemma closureS A B : A `<=` B -> closure A `<=` closure B. Proof. by move=> ? ? CAx ?; move/CAx; exact/subsetI_neq0. Qed. +#[deprecated(since="mathcomp-analysis 1.16.0", use=closureS)] +Definition closure_subset := closureS. + Lemma closureE A : closure A = smallest closed A. Proof. rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closureS AB). From e85ec1b0e98811f06cca506aa8466f8d7ca8ecd7 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 25 Feb 2026 12:13:32 +0900 Subject: [PATCH 3/3] use -> note --- theories/topology_theory/topology_structure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 97e66c029..a8d31bc86 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -843,7 +843,7 @@ Implicit Types E A B U : set T. Lemma closureS A B : A `<=` B -> closure A `<=` closure B. Proof. by move=> ? ? CAx ?; move/CAx; exact/subsetI_neq0. Qed. -#[deprecated(since="mathcomp-analysis 1.16.0", use=closureS)] +#[deprecated(since="mathcomp-analysis 1.16.0", note="Use `closureS` instead.")] Definition closure_subset := closureS. Lemma closureE A : closure A = smallest closed A.