fixes #1926 (#1938)

--
Co-authored-by: Marie Kerjean <marie.kerjean@cnrs.fr>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -109,6 +109,8 @@
   + `Rintegral_itv_bndo_bndc` -> `Rintegral_itvbo_itvbc`
   + `Rintegral_itv_obnd_cbnd` -> `Rintegral_itvob_itvcb`
 
+- in `topology_structure.v`:
+  + `cts_fun` -> `continuous_fun`
 - in `measure_function.v`:
   + `isFinite` -> `isFinNumFun`
 

theories/homotopy_theory/continuous_path.v

@@ -113,14 +113,14 @@ Context (f : {path i from x to y}) (phi : {path j from zero to one in i}).
 *)
 Definition reparameterize := f \o phi.
 
-Local Lemma fphi_zero : reparameterize zero = x.
+#[local] Lemma fphi_zero : reparameterize zero = x.
 Proof. by rewrite /reparameterize /= ?path_zero. Qed.
 
-Local Lemma fphi_one : reparameterize one = y.
+#[loca] Lemma fphi_one : reparameterize one = y.
 Proof. by rewrite /reparameterize /= ?path_one. Qed.
 
-Local Lemma fphi_cts : continuous reparameterize.
-Proof. by move=> ?; apply: continuous_comp; apply: cts_fun. Qed.
+#[local] Lemma fphi_cts : continuous reparameterize.
+Proof. by move=> ?; apply: continuous_comp; exact: continuous_fun. Qed.
 
 HB.instance Definition _ := isContinuous.Build _ _ reparameterize fphi_cts.
 
@@ -156,21 +156,21 @@ Section chain_path.
 Context {T : topologicalType} {i j : bpTopologicalType} (x y z: T).
 Context (p : {path i from x to y}) (q : {path j from y to z}).
 
-Local Lemma chain_path_zero : chain_path p q zero = x.
+#[local] Lemma chain_path_zero : chain_path p q zero = x.
 Proof.
 rewrite /chain_path /= wedge_lift_funE ?path_one ?path_zero //.
 by case => //= [][] //=; rewrite ?path_one ?path_zero.
 Qed.
 
-Local Lemma chain_path_one : chain_path p q one = z.
+#[local] Lemma chain_path_one : chain_path p q one = z.
 Proof.
 rewrite /chain_path /= wedge_lift_funE ?path_zero ?path_one //.
 by case => //= [][] //=; rewrite ?path_one ?path_zero.
 Qed.
 
-Local Lemma chain_path_cts : continuous (chain_path p q).
+#[local] Lemma chain_path_cts : continuous (chain_path p q).
 Proof.
-apply: chain_path_cts_point; [exact: cts_fun..|].
+apply: chain_path_cts_point; [exact: continuous_fun..|].
 by rewrite path_zero path_one.
 Qed.
 

theories/normedtype_theory/tvs.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 all_ssreflect_compat ssralg ssrnum vector.
 From mathcomp Require Import interval_inference.
@@ -779,11 +779,11 @@ Context {R : numDomainType} {E F : NbhsLmodule.type R}
   {S : NbhsZmodule.type} {s : GRing.Scale.law R S}
   (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}).
 
-Let lcfun_comp_subproof1 : linear_for s (g \o f).
+#[local] Lemma lcfun_comp_subproof1 : linear_for s (g \o f).
 Proof. by move=> *; move=> *; rewrite !linearP. Qed.
 
-Let lcfun_comp_subproof2 : continuous (g \o f).
-Proof. by move=> x; apply: continuous_comp; exact/cts_fun. Qed.
+#[local] Lemma lcfun_comp_subproof2 : continuous (g \o f).
+Proof. by move=> x; apply: continuous_comp; exact/continuous_fun. Qed.
 
 HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
   lcfun_comp_subproof1 lcfun_comp_subproof2.
@@ -800,25 +800,25 @@ Proof. by apply: cst_continuous. Qed.
 
 HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
 
-Let lcfun_continuousD f g : continuous (f \+ g).
-Proof. by move=> /= x; apply: fun_cvgD; exact: cts_fun. Qed.
+#[local] Lemma lcfun_continuousD f g : continuous (f \+ g).
+Proof. by move=> /= x; apply: fun_cvgD; exact: continuous_fun. Qed.
 
 HB.instance Definition _ f g :=
   isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
 
-Let lcfun_continuousN f : continuous (\- f).
-Proof. by move=> /= x; apply: fun_cvgN; exact: cts_fun. Qed.
+#[local] Lemma lcfun_continuousN f : continuous (\- f).
+Proof. by move=> /= x; apply: fun_cvgN; exact: continuous_fun. Qed.
 
 HB.instance Definition _ f :=
   isContinuous.Build E F (\- f) (@lcfun_continuousN f).
 
-Let lcfun_continuousM r g : continuous (r \*: g).
-Proof. by move=> /= x; apply: fun_cvgZr; exact: cts_fun. Qed.
+#[local] Lemma lcfun_continuousM r g : continuous (r \*: g).
+Proof. by move=> /= x; apply: fun_cvgZr; exact: continuous_fun. Qed.
 
 HB.instance Definition _ r g :=
   isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g).
 
-Let lcfun_submod_closed : submod_closed (@lcfun R E F *:%R).
+#[local] Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R).
 Proof.
 split; first by rewrite inE; split; first apply/linearP; exact: cst_continuous.
 move=> r /= _ _  /lcfunP[f] /lcfunP[g].
@@ -837,9 +837,9 @@ Section lcfunproperties.
 Context {R : numDomainType} {E F : NbhsLmodule.type R}
   (f : {linear_continuous E -> F}).
 
-#[warn(note="Consider using `cts_fun` instead.",cats="discoverability")]
+#[warn(note="Consider using `continuous_fun` instead.",cats="discoverability")]
 Lemma lcfun_continuous : continuous f.
-Proof. exact: cts_fun. Qed.
+Proof. exact: continuous_fun. Qed.
 
 #[warn(note="Consider using `linearP` instead.",cats="discoverability")]
 Lemma lcfun_linear : linear f.

theories/topology_theory/subspace_topology.v

@@ -701,10 +701,10 @@ Section continuous_fun_comp.
 Context {X Y Z : topologicalType} (A : set X) (B : set Y) (C : set Z).
 Context {f : continuousSubspaceType A B} {g : continuousSubspaceType B C}.
 
-Local Lemma continuous_comp_subproof : continuous (g \o f : subspace A -> Z).
+#[local] Lemma continuous_comp_subproof : continuous (g \o f : subspace A -> Z).
 Proof.
-move=> x; apply: continuous_comp; last exact: cts_fun.
-exact/subspaceT_continuous/cts_fun.
+move=> x; apply: continuous_comp; last exact: continuous_fun.
+exact/subspaceT_continuous/continuous_fun.
 Qed.
 
 HB.instance Definition _ :=

theories/topology_theory/topology_structure.v

@@ -1031,14 +1031,18 @@ End ClopenSets.
 Notation clopen_comp := preimage_clopen (only parsing).
 
 HB.mixin Record isContinuous {X Y : nbhsType} (f : X -> Y):= {
-  cts_fun : continuous f
+  continuous_fun : continuous f
 }.
 
 #[short(type = "continuousType")]
 HB.structure Definition Continuous {X Y : nbhsType} := {
   f of @isContinuous X Y f
 }.
 
+#[deprecated(since="mathcomp-analysis 1.17.0",
+             note="use `continuous_fun` instead")]
+Notation cts_fun := (continuous_fun) (only parsing).
+
 HB.instance Definition _ {X Y : topologicalType} :=
   gen_eqMixin (continuousType X Y).
 HB.instance Definition _ {X Y : topologicalType} :=
@@ -1050,7 +1054,7 @@ Proof.
 case: f g => [f [[ffun]]] [g [[gfun]]]/=; split=> [[->//]|/funext eqfg].
 rewrite eqfg in ffun *; congr {| Continuous.sort := _; Continuous.class := {|
   Continuous.topology_structure_isContinuous_mixin :=
-    {|isContinuous.cts_fun := _|}|}|}.
+    {|isContinuous.continuous_fun := _|}|}|}.
 exact: Prop_irrelevance.
 Qed.
 
@@ -1063,8 +1067,8 @@ Section continuous_comp.
 Context {X Y Z : topologicalType}.
 Context (f : continuousType X Y) (g : continuousType Y Z).
 
-Local Lemma cts_fun_comp : continuous (g \o f).
-Proof. move=> x; apply: continuous_comp; exact: cts_fun. Qed.
+#[local] Lemma cts_fun_comp : continuous (g \o f).
+Proof. move=> x; apply: continuous_comp; exact: continuous_fun. Qed.
 
 HB.instance Definition _ := @isContinuous.Build X Z (g \o f) cts_fun_comp.
 
@@ -1073,7 +1077,7 @@ End continuous_comp.
 Section continuous_id.
 Context {X : topologicalType}.
 
-Local Lemma cts_id : continuous (@idfun X).
+#[local] Lemma cts_id : continuous (@idfun X).
 Proof. by move=> ?. Qed.
 
 HB.instance Definition _ := @isContinuous.Build X X (@idfun X) cts_id.
@@ -1083,7 +1087,7 @@ End continuous_id.
 Section continuous_const.
 Context {X Y : topologicalType} (y : Y).
 
-Local Lemma cts_const : continuous (@cst X Y y).
+#[local] Lemma cts_const : continuous (@cst X Y y).
 Proof. by move=> ?; exact: cvg_cst. Qed.
 
 HB.instance Definition _ := @isContinuous.Build X Y (cst y) cts_const.