From 1b1360bf047d633a4545834c53881df7afd66ca3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 18 Apr 2026 17:41:03 +0900 Subject: [PATCH] fixes #1926 --- CHANGELOG_UNRELEASED.md | 2 ++ theories/homotopy_theory/continuous_path.v | 16 ++++++------ theories/normedtype_theory/tvs.v | 26 +++++++++---------- theories/topology_theory/subspace_topology.v | 6 ++--- theories/topology_theory/topology_structure.v | 16 +++++++----- 5 files changed, 36 insertions(+), 30 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ba0f99048..3aa617ab4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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` ### Generalized diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index 367f927c4..b10955873 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/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. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index bdc1d4c2c..00b1a3385 100644 --- a/theories/normedtype_theory/tvs.v +++ b/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. diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 0565b3413..36019a2d0 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/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 _ := diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index e16cf5318..3733d9de2 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -1031,7 +1031,7 @@ 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")] @@ -1039,6 +1039,10 @@ 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.