fix #1843

CHANGELOG_UNRELEASED.md

@@ -195,6 +195,10 @@
 - in `lebesgue_integral_nonneg.v`:
   + `integral_setD1_EFin` -> `integral_setD1`
 
+- in `topology_structure.v`:
+  + `closed_comp` -> `preimage_closed`
+  + `clopen_comp` -> `preimage_clopen`
+
 ### Generalized
 
 - in `lebesgue_integral_nonneg.v`:

theories/function_spaces.v

@@ -1,6 +1,7 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap generic_quotient.
+From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import generic_quotient.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
@@ -291,7 +292,7 @@ Proof.
 move=> dctTI x y /eqP xneqy.
 have [i/eqP/dctTI [U [clU Ux nUy]]] : exists i, x i <> y i.
   by apply/existsNP=> W; exact/xneqy/functional_extensionality_dep.
-exists (proj i @^-1` U); split => //; apply: clopen_comp => //.
+exists (proj i @^-1` U); split => //; apply: preimage_clopen => //.
 exact/proj_continuous.
 Qed.
 

theories/normedtype_theory/normed_module.v

@@ -2018,7 +2018,7 @@ Lemma closed_closed_ball_ (R : realFieldType) (V : normedModType R)
   (x : V) (e : R) : closed (closed_ball_ normr x e).
 Proof.
 rewrite /closed_ball_ -/((normr \o (fun y => x - y)) @^-1` [set x | x <= e]).
-apply: (closed_comp _ (@closed_le _ _)) => y _.
+apply: (preimage_closed _ (@closed_le _ _)) => y _.
 apply: (continuous_comp _ (@norm_continuous _ _ _)).
 exact: (continuousB (@cst_continuous _ _ _ _)).
 Qed.

theories/numfun.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 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 all_ssreflect_compat ssralg ssrnum ssrint interval finmap.
 #[warning="-warn-library-file-internal-analysis"]
@@ -1117,8 +1117,8 @@ Proof.
 move: M => _/posnumP[M] ctsf fA1.
 have [] := @urysohn_ext_itv (A `&` f @^-1` `]-oo, -(1/3) * M%:num])
     (A `&` f @^-1` `[1/3 * M%:num,+oo[) (-(1/3) * M%:num) (1/3 * M%:num).
-- by rewrite closed_setSI//; exact: closed_comp.
-- by rewrite closed_setSI//; apply: closed_comp => //; exact: interval_closed.
+- by rewrite closed_setSI//; exact: preimage_closed.
+- by rewrite closed_setSI//; apply: preimage_closed => //; exact: interval_closed.
 - rewrite setIACA -preimage_setI eqEsubset; split => z // [_ []].
   rewrite !set_itvE/= => /[swap] /le_trans /[apply].
   by rewrite leNgt mulNr gtrN// mulr_gt0// divr_gt0.

theories/topology_theory/subspace_topology.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 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 all_ssreflect_compat all_algebra all_classical.
 From mathcomp Require Import topology_structure uniform_structure compact.
@@ -627,7 +627,7 @@ have [fAfE cEIE] :
 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: closed_comp => //; exact: closed_closure.
+      by apply: preimage_closed => //; exact: closed_closure.
     apply: closure_subset.
     have /(@preimage_subset _ _ f) A0cA0 := @subset_closure _ (E b).
     by apply: subset_trans A0cA0; apply: subIset; right.

theories/topology_theory/topology_structure.v

@@ -784,7 +784,7 @@ 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) :
+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.
@@ -793,6 +793,8 @@ have NDfx : ~ D (f x).
   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`")]
+Notation closed_comp := preimage_closed (only parsing).
 
 Lemma closed_cvg {T} {V : topologicalType} {F} {FF : ProperFilter F}
     (u_ : T -> V) (A : V -> Prop) :
@@ -1006,11 +1008,13 @@ Proof. by split; [exact: open0 | exact: closed0]. Qed.
 Lemma clopenT {T} : clopen [set: T].
 Proof. by split; [exact: openT | exact: closedT]. Qed.
 
-Lemma clopen_comp {T U : topologicalType} (f : T -> U) (A : set U) :
+Lemma preimage_clopen {T U : topologicalType} (f : T -> U) (A : set U) :
  clopen A -> continuous f -> clopen (f @^-1` A).
-Proof. by case=> ? ?; split; [ exact: open_comp | exact: closed_comp]. Qed.
+Proof. by case=> ? ?; split; [ exact: open_comp | exact: preimage_closed]. Qed.
 
 End ClopenSets.
+#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `preimage_clopen`")]
+Notation clopen_comp := preimage_clopen (only parsing).
 
 HB.mixin Record isContinuous {X Y : nbhsType} (f : X -> Y):= {
   cts_fun : continuous f