fix #1849 (closure_subset -> closureS) (#1857)

* rename closure_subset -> closureS; add interiorS

Author: t6s

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`

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].

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 :

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`")]

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.

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) :

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.
 

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.

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.

theories/topology_theory/topology_structure.v

@@ -840,12 +840,15 @@ 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.
 
+#[deprecated(since="mathcomp-analysis 1.16.0", note="Use `closureS` instead.")]
+Definition closure_subset := closureS.
+
 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 +889,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->].