Skip to content

fixes #1926 (cts_fun renaming) #1938

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
affeldt-aist merged 2 commits into from
Apr 22, 2026
Merged

fixes #1926 (cts_fun renaming) #1938

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1b1360b
fixes #1926
affeldt-aist Apr 18, 2026
461d5cd
Merge branch 'master' into topology_20260418
affeldt-aist Apr 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`

Expand Down
16 changes: 8 additions & 8 deletions theories/homotopy_theory/continuous_path.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.

Expand Down
26 changes: 13 additions & 13 deletions theories/normedtype_theory/tvs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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].
Expand All @@ -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.
Expand Down
6 changes: 3 additions & 3 deletions theories/topology_theory/subspace_topology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ :=
Expand Down
16 changes: 10 additions & 6 deletions theories/topology_theory/topology_structure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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} :=
Expand All @@ -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.

Expand All @@ -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.

Expand All @@ -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.
Expand All @@ -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.
Expand Down
Loading