From 593c96958519c2bfc1d296c51525e16dd28ec60c Mon Sep 17 00:00:00 2001
From: mkerjean <marie.kerjean@lipn.univ-paris13.fr>
Date: Fri, 20 Mar 2026 11:14:19 +0900
Subject: [PATCH 01/12] linfun and lcfun are lmodtypes

Co-authored-by: Cyril Cohen <cohen@crans.org>
---
 classical/functions.v            | 117 ++++++++++++++++++
 theories/normedtype_theory/tvs.v | 202 ++++++++++++++++++++++++++++++-
 2 files changed, 315 insertions(+), 4 deletions(-)

diff --git a/classical/functions.v b/classical/functions.v
index 77be38a0a..ee2b1972a 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -128,6 +128,12 @@ Add Search Blacklist "_mixin_".
 (*                   fctE == multi-rule for fct                               *)
 (* ```                                                                        *)
 (*                                                                            *)
+(* ```                                                                        *)
+(*Section linfun_lmodtype == canonical lmodtype structure on linear maps      *)
+(*                           between lmodtypes.                               *)
+(*                                                                            *)
+(*                                                                            *)
+(*                                                                            *)
 (******************************************************************************)
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
@@ -2750,3 +2756,114 @@ End function_space_lemmas.
 
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
+
+(* TODO : correct - choicetype on {linear _ -> _} is no longer seen, cf bug in
+derive.v when uncommenting *)
+
+(*
+Local Open Scope ring_scope.
+Import GRing.Theory.
+
+Section linfun_pred.
+(* Beware that lfun is reserved for vector types, hence this one has been
+renamed linfun *)
+Context  {K : numDomainType} {E : lmodType K}  {F : lmodType K} {s : K -> F -> F}.
+Definition linfun : {pred E -> F} := mem [set f | linear_for s f ].
+Definition linfun_key : pred_key linfun. Proof. exact. Qed.
+Canonical linfun_keyed := KeyedPred linfun_key.
+
+End linfun_pred.
+
+Section linfun.
+Context {R : numDomainType} {E : lmodType R}
+  {F : lmodType R} {s : GRing.Scale.law R F}.
+Notation T := {linear E -> F | s}.
+Notation linfun := (@linfun _ E F s).
+
+Section Sub.
+Context (f : E -> F) (fP : f \in linfun).
+
+Definition linfun_Sub_subproof :=
+  @GRing.isLinear.Build _ E F s f  (set_mem fP).
+
+#[local] HB.instance Definition _ := linfun_Sub_subproof.
+Definition linfun_Sub : {linear _  -> _ | _ } := f.
+End Sub.
+
+Lemma linfun_rect (K : T -> Type) :
+  (forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u.
+Proof.
+move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
+set G := (G in K G).
+have Pf : f \in linfun.
+  by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
+suff -> : G = linfun_Sub Pf by apply: Ksub.
+rewrite {}/G.
+congr GRing.Linear.Pack. 
+congr GRing.Linear.Class.
+- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance. 
+- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
+Qed.
+
+Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
+
+Lemma linfuneqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+
+HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
+
+Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
+  | Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
+
+(*to be renamed ?*)
+Lemma linfunE (f : E -> F) : (f \in linfun) -> linfun_spec f f (f \in linfun).
+Proof.
+move=> /[dup] f_lc ->.
+have {2}-> :(f = (linfun_Sub f_lc)) by rewrite linfun_valP.
+constructor.
+Qed.
+
+End linfun.
+
+Section linfun_comp.
+
+Context {R : numDomainType} {E F : lmodType R}
+  {S : lmodType R} {s : GRing.Scale.law R S}
+  (f : {linear E -> F}) (g : {linear F -> S | s}).
+
+Lemma linfun_comp_subproof : linear_for s (g \o f). 
+Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
+
+HB.instance Definition _ := @GRing.isLinear.Build R E S s (g \o f)
+  linfun_comp_subproof.  
+(* HB warning : no new instance generated but before we have 
+Fail Check ( (g \o f) : {linear E -> F | s}). ? *)
+
+End linfun_comp.
+
+Section linfun_lmodtype.
+Context {R : numFieldType} {E F G: lmodType R}. 
+
+Implicit Types (r : R) (f g : {linear E -> F}) (h : {linear F -> G}).  
+
+Import GRing.Theory.
+
+Lemma linfun0 : (\0 : {linear E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed.
+
+Lemma linfun_submod_closed  : submod_closed (@linfun R E F *:%R).
+Proof.
+split; first by rewrite inE; apply/linearP.  
+move=> r /= _ _  /linfunE[f] /linfunE[g].
+by rewrite inE /=; exact: linearP.
+Qed. 
+ 
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _ linfun linfun_submod_closed.
+
+HB.instance Definition _ :=
+  [SubChoice_isSubLmodule of {linear E -> F } by <:].
+
+End linfun_lmodtype.*)
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 7ba894e04..2e0523064 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) 2017 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.
@@ -37,10 +37,10 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (*           UniformZmodule == HB class, join of UniformNmodule and Zmodule   *)
 (*                             with uniformly continuous opposite operator    *)
 (*      PreUniformLmodule K == HB class, join of Uniform and Lmodule over K   *)
-(*                             K is a numDomainType.                          *)
+(*                             K is a numDomainType                           *)
 (*         UniformLmodule K == HB class, join of UniformNmodule and Lmodule   *)
 (*                             with a uniformly continuous scaling operation  *)
-(*                             K is a numFieldType.                           *)
+(*                             K is a numFieldType                            *)
 (*         convexTvsType R  == interface type for a locally convex            *)
 (*                             tvs on a numDomain R                           *)
 (*                             A convex tvs is constructed over a uniform     *)
@@ -49,7 +49,6 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a   *)
 (*                             convex tvs from an Lmodule which is also a     *)
 (*                             topological space                              *)
-(*  ```                                                                       *)
 (* HB instances:                                                              *)
 (* - The type R^o (R : numFieldType) is endowed with the structure of         *)
 (*   ConvexTvs.                                                               *)
@@ -603,3 +602,198 @@ HB.instance Definition _ :=
   Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex.
 
 End prod_ConvexTvs.
+
+HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
+  (F : NbhsZmodule.type) (s : K -> F -> F) :=
+  {f of @GRing.Linear K E F s f &  @Continuous E F f }.
+
+(* https://github.com/math-comp/math-comp/issues/1536
+   we use GRing.Scale.law even though it is claimed to be internal *)
+HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
+  (F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := {
+    linearP : linear_for s f ;
+    continuousP : continuous f
+  }.
+
+HB.builders Context K E F s f of @isLinearContinuous K E F s f.
+
+HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP.
+HB.instance Definition _ := isContinuous.Build E F f continuousP.
+
+HB.end.
+
+Section lcfun_pred.
+Context  {K : numDomainType} {E : NbhsLmodule.type K}  {F : NbhsZmodule.type} {s : K -> F -> F}.
+Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ].
+Definition lcfun_key : pred_key lcfun. Proof. exact. Qed.
+Canonical lcfun_keyed := KeyedPred lcfun_key.
+
+End lcfun_pred.
+
+Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
+  (at level 0, U at level 98, V at level 99,
+   format "{ 'linear_continuous'  U  ->  V  |  s }").
+Reserved Notation "'{' 'linear_continuous' U '->' V '}'"
+  (at level 0, U at level 98, V at level 99,
+   format "{ 'linear_continuous'  U  ->  V }").
+Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s)
+  : type_scope.
+Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
+  : type_scope.
+  
+Section lcfun.
+Context {R : numDomainType} {E : NbhsLmodule.type R}
+  {F : NbhsZmodule.type} {s : GRing.Scale.law R F}.
+Notation T := {linear_continuous E -> F | s}.
+Notation lcfun := (@lcfun _ E F s).
+
+Section Sub.
+Context (f : E -> F) (fP : f \in lcfun).
+  
+Definition lcfun_Sub_subproof :=
+  @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)).
+#[local] HB.instance Definition _ := lcfun_Sub_subproof.
+Definition lcfun_Sub : {linear_continuous _  -> _ | _ } := f.
+End Sub.
+
+Lemma lcfun_rect (K : T -> Type) :
+  (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u.
+Proof.
+move=> Ksub [f [[Pf1] [Pf2] [Pf3]]].
+set G := (G in K G).
+have Pf : f \in lcfun.
+  by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2.
+suff -> : G = lcfun_Sub Pf by apply: Ksub.
+rewrite {}/G.
+congr LinearContinuous.Pack.
+congr LinearContinuous.Class.
+- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
+- by congr isContinuous.Axioms_; apply: Prop_irrelevance.
+Qed.
+
+Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP.
+
+Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+
+HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:].
+
+Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
+  | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
+
+(*to be renamed ?*)
+Lemma lcfunE (f : E -> F) : (f \in lcfun) -> lcfun_spec f f (f \in lcfun).
+Proof.
+move=> /[dup] f_lc ->.
+have {2}-> :(f = (lcfun_Sub f_lc)) by rewrite lcfun_valP.
+constructor.
+Qed.
+
+End lcfun.
+
+Section lcfun_comp.
+
+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}).
+
+Lemma lcfun_comp_subproof1 : linear_for s (g \o f). 
+Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
+
+(* TODO weaken proof continuous_comp to arbitrary nbhsType *)
+Lemma lcfun_comp_subproof2 : continuous (g \o f). 
+Proof. by move=> x; move=> A /cts_fun /cts_fun. Qed.
+
+HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
+  lcfun_comp_subproof1 lcfun_comp_subproof2.
+
+End lcfun_comp.
+
+Section lcfun_lmodtype.
+Context {R : numFieldType} {E F G: convexTvsType R}. 
+
+Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}).  
+
+Import GRing.Theory.
+
+Lemma null_fun_continuous : continuous (\0 : E -> F).
+Proof.
+by apply: cst_continuous.
+Qed.
+
+HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
+
+Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _).
+Proof. by []. Qed.
+
+(* NB : cvgD in pseudometric_normedZmodule should be lowered to some common
+structure to tvstype and pseudometric, then lcfun doesn't need to exist
+anymore *)
+Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
+  f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
+Proof.
+move=> fa ga.
+apply: continuous2_cvg; [|by []..].
+apply @add_continuous. (* TODO: why the @ ? *)
+Qed.
+
+Lemma lcfun_continuousD f g : continuous (f \+ g).
+Proof. move=> /= x; apply: lcfun_cvgD; apply: cts_fun. Qed.
+
+
+Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a : f @ U --> a -> \- f @ U --> - a.
+Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
+
+
+Lemma lcfun_continuousN f : continuous (\- f).
+Proof.
+by move=> /= x; apply: lcfun_cvgN; apply: cts_fun. 
+Qed.
+
+HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
+
+Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a : l @ U  --> r -> f @ U --> a ->
+                     l x *: f x @[x --> U] --> r *: a.
+Proof.
+move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
+Qed.
+
+Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a.
+Proof. apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
+
+Lemma lcfun_continuousM r g : continuous (r \*: g).
+Proof. by move=> /= x; apply: lcfun_cvgZr; apply: cts_fun. Qed.
+
+HB.instance Definition _ r g := isContinuous.Build E F (r \*: g)  (@lcfun_continuousM r g).
+
+Lemma lcfun_submod_closed  : submod_closed (@lcfun R E F *:%R).
+Proof.
+split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous.
+move=> r /= _ _  /lcfunE[f] /lcfunE[g].
+by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD].
+Qed.
+
+HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f).
+
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _ lcfun lcfun_submod_closed.
+
+HB.instance Definition _ :=
+  [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
+
+End lcfun_lmodtype.
+
+
+Section Substructures.
+Context (R: numFieldType) (V : convexTvsType R).
+Variable (A : pred V).
+
+HB.instance Definition _ := ConvexTvs.on (subspace A).
+
+Check {linear_continuous (subspace A) -> R^o}.
+
+End Substructures.

From f21d13e773bc042e5925fe685f65afefb062f514 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 25 Mar 2026 12:20:15 +0900
Subject: [PATCH 02/12] uncomment and make compile

---
 CHANGELOG_UNRELEASED.md                       |   9 ++
 classical/classical_sets.v                    |  11 ++
 classical/filter.v                            |   5 +
 classical/functions.v                         |  65 ++++--------
 theories/normedtype_theory/tvs.v              | 100 ++++++++----------
 theories/topology_theory/topology_structure.v |   5 -
 6 files changed, 89 insertions(+), 106 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1b864bc1d..aaed55eed 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,8 +4,17 @@
 
 ### Added
 
+- in `functions.v`:
+  + mixin ...
+
+- in `tvs.v`:
+  + ...
+
 ### Changed
 
+- moved from `topology_structure.v` to `filter.v`:
+  + lemma `continuous_comp` (and generalized)
+
 ### Renamed
 
 - in `tvs.v`:
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index a2522509f..56539395a 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -2463,6 +2463,17 @@ HB.instance Definition _ m n (T : pointedType) :=
 HB.instance Definition _ (T : choiceType) := isPointed.Build (option T) None.
 HB.instance Definition _ (T : choiceType) := isPointed.Build {fset T} fset0.
 
+HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
+  isPointed.Build {linear E -> F} (Algebra.null_fun _).
+
+(*Section coucou.
+Context {R : numDomainType} (E F : lmodType R).
+
+Check (point : {linear E -> F}%R).*)
+
+
+
+
 Notation get := (xget point).
 Notation "[ 'get' x | E ]" := (get [set x | E])
   (at level 0, x name, format "[ 'get'  x  |  E ]", only printing) : form_scope.
diff --git a/classical/filter.v b/classical/filter.v
index 0cd56cf06..33096e489 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -946,6 +946,11 @@ Definition continuous_at (T U : nbhsType) (x : T) (f : T -> U) :=
   (f%function @ x --> f%function x).
 Notation continuous f := (forall x, continuous_at x f).
 
+Lemma continuous_comp (R S T : nbhsType) (f : R -> S) (g : S -> T) x :
+  {for x, continuous f} -> {for (f x), continuous g} ->
+  {for x, continuous (g \o f)}.
+Proof. exact: cvg_comp. Qed.
+
 Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) :
     {for x, continuous f} ->
   (\forall y \near f x, P y) -> (\near x, P (f x)).
diff --git a/classical/functions.v b/classical/functions.v
index ee2b1972a..8f6b2df18 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2757,17 +2757,15 @@ End function_space_lemmas.
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
 
-(* TODO : correct - choicetype on {linear _ -> _} is no longer seen, cf bug in
-derive.v when uncommenting *)
-
-(*
 Local Open Scope ring_scope.
 Import GRing.Theory.
 
 Section linfun_pred.
-(* Beware that lfun is reserved for vector types, hence this one has been
-renamed linfun *)
-Context  {K : numDomainType} {E : lmodType K}  {F : lmodType K} {s : K -> F -> F}.
+Context {K : numDomainType} {E : lmodType K}  {F : lmodType K}
+  {s : K -> F -> F}.
+
+(**md Beware that `lfun` is reserved for vector types, hence this one has been
+ named `linfun` *)
 Definition linfun : {pred E -> F} := mem [set f | linear_for s f ].
 Definition linfun_key : pred_key linfun. Proof. exact. Qed.
 Canonical linfun_keyed := KeyedPred linfun_key.
@@ -2795,14 +2793,12 @@ Lemma linfun_rect (K : T -> Type) :
 Proof.
 move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
 set G := (G in K G).
-have Pf : f \in linfun.
-  by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
+have Pf : f \in linfun by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
 suff -> : G = linfun_Sub Pf by apply: Ksub.
 rewrite {}/G.
-congr GRing.Linear.Pack. 
-congr GRing.Linear.Class.
-- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance. 
-- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
+congr (GRing.Linear.Pack (GRing.Linear.Class _ _)).
+- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance.
 Qed.
 
 Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
@@ -2818,52 +2814,35 @@ HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
 Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
   | Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
 
-(*to be renamed ?*)
-Lemma linfunE (f : E -> F) : (f \in linfun) -> linfun_spec f f (f \in linfun).
+Lemma linfunP (f : E -> F) : f \in linfun -> linfun_spec f f (f \in linfun).
 Proof.
 move=> /[dup] f_lc ->.
-have {2}-> :(f = (linfun_Sub f_lc)) by rewrite linfun_valP.
-constructor.
+have {2}-> : f = linfun_Sub f_lc by rewrite linfun_valP.
+by constructor.
 Qed.
 
 End linfun.
 
-Section linfun_comp.
-
-Context {R : numDomainType} {E F : lmodType R}
-  {S : lmodType R} {s : GRing.Scale.law R S}
-  (f : {linear E -> F}) (g : {linear F -> S | s}).
-
-Lemma linfun_comp_subproof : linear_for s (g \o f). 
-Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
-
-HB.instance Definition _ := @GRing.isLinear.Build R E S s (g \o f)
-  linfun_comp_subproof.  
-(* HB warning : no new instance generated but before we have 
-Fail Check ( (g \o f) : {linear E -> F | s}). ? *)
-
-End linfun_comp.
-
 Section linfun_lmodtype.
-Context {R : numFieldType} {E F G: lmodType R}. 
-
-Implicit Types (r : R) (f g : {linear E -> F}) (h : {linear F -> G}).  
+Context {R : numFieldType} {E F : lmodType R}.
 
 Import GRing.Theory.
 
-Lemma linfun0 : (\0 : {linear E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed.
-
 Lemma linfun_submod_closed  : submod_closed (@linfun R E F *:%R).
 Proof.
-split; first by rewrite inE; apply/linearP.  
-move=> r /= _ _  /linfunE[f] /linfunE[g].
+split; first by rewrite inE; exact/linearP.
+move=> r /= _ _ /linfunP[f] /linfunP[g].
 by rewrite inE /=; exact: linearP.
-Qed. 
- 
+Qed.
+
 HB.instance Definition _ :=
   @GRing.isSubmodClosed.Build _  _ linfun linfun_submod_closed.
 
 HB.instance Definition _ :=
   [SubChoice_isSubLmodule of {linear E -> F } by <:].
 
-End linfun_lmodtype.*)
+End linfun_lmodtype.
+
+(* TODO: we wanted to declare this instance in classical_sets.v but failed and did not understand why, also we couldn't generaliz *)
+HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
+  isPointed.Build {linear E -> F} (\0)%R.
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 2e0523064..0b6121b3b 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) 2017 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.
@@ -640,7 +640,7 @@ Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%typ
   : type_scope.
 Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
   : type_scope.
-  
+
 Section lcfun.
 Context {R : numDomainType} {E : NbhsLmodule.type R}
   {F : NbhsZmodule.type} {s : GRing.Scale.law R F}.
@@ -649,7 +649,7 @@ Notation lcfun := (@lcfun _ E F s).
 
 Section Sub.
 Context (f : E -> F) (fP : f \in lcfun).
-  
+
 Definition lcfun_Sub_subproof :=
   @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)).
 #[local] HB.instance Definition _ := lcfun_Sub_subproof.
@@ -665,11 +665,10 @@ have Pf : f \in lcfun.
   by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2.
 suff -> : G = lcfun_Sub Pf by apply: Ksub.
 rewrite {}/G.
-congr LinearContinuous.Pack.
-congr LinearContinuous.Class.
-- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance.
-- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
-- by congr isContinuous.Axioms_; apply: Prop_irrelevance.
+congr (LinearContinuous.Pack (LinearContinuous.Class _ _ _)).
+- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance.
+- by congr isContinuous.Axioms_; exact: Prop_irrelevance.
 Qed.
 
 Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
@@ -685,12 +684,11 @@ HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:].
 Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
   | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
 
-(*to be renamed ?*)
-Lemma lcfunE (f : E -> F) : (f \in lcfun) -> lcfun_spec f f (f \in lcfun).
+Lemma lcfunP (f : E -> F) : f \in lcfun -> lcfun_spec f f (f \in lcfun).
 Proof.
 move=> /[dup] f_lc ->.
-have {2}-> :(f = (lcfun_Sub f_lc)) by rewrite lcfun_valP.
-constructor.
+have {2}-> : f = lcfun_Sub f_lc by rewrite lcfun_valP.
+by constructor.
 Qed.
 
 End lcfun.
@@ -701,12 +699,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}).
 
-Lemma lcfun_comp_subproof1 : linear_for s (g \o f). 
-Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
+Let lcfun_comp_subproof1 : linear_for s (g \o f).
+Proof. by move=> *; move=> *; rewrite !linearP. Qed.
 
-(* TODO weaken proof continuous_comp to arbitrary nbhsType *)
-Lemma lcfun_comp_subproof2 : continuous (g \o f). 
-Proof. by move=> x; move=> A /cts_fun /cts_fun. Qed.
+Let lcfun_comp_subproof2 : continuous (g \o f).
+Proof. by move=> x; apply: continuous_comp; exact/cts_fun. Qed.
 
 HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
   lcfun_comp_subproof1 lcfun_comp_subproof2.
@@ -714,9 +711,8 @@ HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
 End lcfun_comp.
 
 Section lcfun_lmodtype.
-Context {R : numFieldType} {E F G: convexTvsType R}. 
-
-Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}).  
+Context {R : numFieldType} {E F : convexTvsType R}.
+Implicit Types (r : R) (f g : {linear_continuous E -> F}).
 
 Import GRing.Theory.
 
@@ -727,57 +723,56 @@ Qed.
 
 HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
 
-Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _).
-Proof. by []. Qed.
-
-(* NB : cvgD in pseudometric_normedZmodule should be lowered to some common
-structure to tvstype and pseudometric, then lcfun doesn't need to exist
-anymore *)
+(** NB : cvgD in pseudometric_normedZmodule could be lowered to some common
+  structure to convexTvsType and pseudometric, then `lcfun_cvgD` doesn't need to
+  exist anymore (we are however not sure that this deserves the introduction of
+  a new structure that combines nbhs and normedZmodule) *)
 Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
   f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
 Proof.
 move=> fa ga.
-apply: continuous2_cvg; [|by []..].
-apply @add_continuous. (* TODO: why the @ ? *)
+by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..].
 Qed.
 
 Lemma lcfun_continuousD f g : continuous (f \+ g).
-Proof. move=> /= x; apply: lcfun_cvgD; apply: cts_fun. Qed.
-
+Proof. by move=> /= x; apply: lcfun_cvgD; exact: cts_fun. Qed.
 
-Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a : f @ U --> a -> \- f @ U --> - a.
+Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a :
+  f @ U --> a -> \- f @ U --> - a.
 Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
 
-
 Lemma lcfun_continuousN f : continuous (\- f).
-Proof.
-by move=> /= x; apply: lcfun_cvgN; apply: cts_fun. 
-Qed.
+Proof. by move=> /= x; apply: lcfun_cvgN; exact: cts_fun. Qed.
 
-HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
+HB.instance Definition _ f g :=
+  isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
 
-Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a : l @ U  --> r -> f @ U --> a ->
-                     l x *: f x @[x --> U] --> r *: a.
+Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a :
+  l @ U  --> r -> f @ U --> a ->
+  l x *: f x @[x --> U] --> r *: a.
 Proof.
-move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
+by move=> *; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
 Qed.
 
-Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a.
-Proof. apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
+Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a :
+  f @ U --> a -> k \*: f @ U --> k *: a.
+Proof. by apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
 
 Lemma lcfun_continuousM r g : continuous (r \*: g).
-Proof. by move=> /= x; apply: lcfun_cvgZr; apply: cts_fun. Qed.
+Proof. by move=> /= x; apply: lcfun_cvgZr; exact: cts_fun. Qed.
 
-HB.instance Definition _ r g := isContinuous.Build E F (r \*: g)  (@lcfun_continuousM r g).
+HB.instance Definition _ r g :=
+  isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g).
 
-Lemma lcfun_submod_closed  : submod_closed (@lcfun R E F *:%R).
+Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R).
 Proof.
-split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous.
-move=> r /= _ _  /lcfunE[f] /lcfunE[g].
+split; first by rewrite inE; split; first apply/linearP; exact: cst_continuous.
+move=> r /= _ _  /lcfunP[f] /lcfunP[g].
 by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD].
 Qed.
 
-HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f).
+HB.instance Definition _ f :=
+  isContinuous.Build E F (\- f) (@lcfun_continuousN f).
 
 HB.instance Definition _ :=
   @GRing.isSubmodClosed.Build _  _ lcfun lcfun_submod_closed.
@@ -786,14 +781,3 @@ HB.instance Definition _ :=
   [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
 
 End lcfun_lmodtype.
-
-
-Section Substructures.
-Context (R: numFieldType) (V : convexTvsType R).
-Variable (A : pred V).
-
-HB.instance Definition _ := ConvexTvs.on (subspace A).
-
-Check {linear_continuous (subspace A) -> R^o}.
-
-End Substructures.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index 1c4b0db96..e49f10041 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -260,11 +260,6 @@ move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA].
 by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA].
 Qed.
 
-Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x :
-  {for x, continuous f} -> {for (f x), continuous g} ->
-  {for x, continuous (g \o f)}.
-Proof. exact: cvg_comp. Qed.
-
 Lemma open_comp  {T U : topologicalType} (f : T -> U) (D : set U) :
   {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D).
 Proof.

From 49a95139f16b3d9d2b26236a2a17303d7e795615 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Wed, 25 Mar 2026 12:24:44 +0900
Subject: [PATCH 03/12] Apply suggestion from @affeldt-aist

---
 theories/normedtype_theory/tvs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 0b6121b3b..f6daebec4 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -37,7 +37,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (*           UniformZmodule == HB class, join of UniformNmodule and Zmodule   *)
 (*                             with uniformly continuous opposite operator    *)
 (*      PreUniformLmodule K == HB class, join of Uniform and Lmodule over K   *)
-(*                             K is a numDomainType                           *)
+(*                             K is a numDomainType.                          *)
 (*         UniformLmodule K == HB class, join of UniformNmodule and Lmodule   *)
 (*                             with a uniformly continuous scaling operation  *)
 (*                             K is a numFieldType                            *)

From 9a456bd90206134a9d082dfbfee5176ce92afad8 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Wed, 25 Mar 2026 12:24:59 +0900
Subject: [PATCH 04/12] Apply suggestion from @affeldt-aist

---
 theories/normedtype_theory/tvs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index f6daebec4..b73fc9537 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -40,7 +40,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (*                             K is a numDomainType.                          *)
 (*         UniformLmodule K == HB class, join of UniformNmodule and Lmodule   *)
 (*                             with a uniformly continuous scaling operation  *)
-(*                             K is a numFieldType                            *)
+(*                             K is a numFieldType.                           *)
 (*         convexTvsType R  == interface type for a locally convex            *)
 (*                             tvs on a numDomain R                           *)
 (*                             A convex tvs is constructed over a uniform     *)

From 24234bcf1375beb6ca440df520beda212a143b4a Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 25 Mar 2026 12:28:20 +0900
Subject: [PATCH 05/12] fix

---
 classical/classical_sets.v | 11 -----------
 classical/functions.v      |  2 +-
 2 files changed, 1 insertion(+), 12 deletions(-)

diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 56539395a..a2522509f 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -2463,17 +2463,6 @@ HB.instance Definition _ m n (T : pointedType) :=
 HB.instance Definition _ (T : choiceType) := isPointed.Build (option T) None.
 HB.instance Definition _ (T : choiceType) := isPointed.Build {fset T} fset0.
 
-HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
-  isPointed.Build {linear E -> F} (Algebra.null_fun _).
-
-(*Section coucou.
-Context {R : numDomainType} (E F : lmodType R).
-
-Check (point : {linear E -> F}%R).*)
-
-
-
-
 Notation get := (xget point).
 Notation "[ 'get' x | E ]" := (get [set x | E])
   (at level 0, x name, format "[ 'get'  x  |  E ]", only printing) : form_scope.
diff --git a/classical/functions.v b/classical/functions.v
index 8f6b2df18..c68e035f8 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2782,7 +2782,7 @@ Section Sub.
 Context (f : E -> F) (fP : f \in linfun).
 
 Definition linfun_Sub_subproof :=
-  @GRing.isLinear.Build _ E F s f  (set_mem fP).
+  @GRing.isLinear.Build _ E F s f (set_mem fP).
 
 #[local] HB.instance Definition _ := linfun_Sub_subproof.
 Definition linfun_Sub : {linear _  -> _ | _ } := f.

From 70f48e5aba4c563e266136f9faac6bf1fbbcb747 Mon Sep 17 00:00:00 2001
From: mkerjean <marie.kerjean@lipn.univ-paris13.fr>
Date: Fri, 27 Mar 2026 21:11:14 +0900
Subject: [PATCH 06/12] notations

---
 theories/normedtype_theory/tvs.v | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index b73fc9537..fc89c61a7 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) 2017 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.
@@ -55,6 +55,13 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (* - The product of two Tvs is endowed with the structure of ConvexTvs.       *)
 (******************************************************************************)
 
+Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
+  (at level 0, U at level 98, V at level 99,
+   format "{ 'linear_continuous'  U  ->  V  |  s }").
+Reserved Notation "'{' 'linear_continuous' U '->' V '}'"
+  (at level 0, U at level 98, V at level 99,
+    format "{ 'linear_continuous'  U  ->  V }"). 
+
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -630,12 +637,6 @@ Canonical lcfun_keyed := KeyedPred lcfun_key.
 
 End lcfun_pred.
 
-Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
-  (at level 0, U at level 98, V at level 99,
-   format "{ 'linear_continuous'  U  ->  V  |  s }").
-Reserved Notation "'{' 'linear_continuous' U '->' V '}'"
-  (at level 0, U at level 98, V at level 99,
-   format "{ 'linear_continuous'  U  ->  V }").
 Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s)
   : type_scope.
 Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
@@ -781,3 +782,15 @@ HB.instance Definition _ :=
   [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
 
 End lcfun_lmodtype.
+
+Section lcfunproperties.
+Context {R : numDomainType} {E F : NbhsLmodule.type R}
+  (f : {linear_continuous E -> F}).
+
+Lemma lcfun_continuous : continuous f. 
+Proof. exact: cts_fun. Qed.
+
+Lemma lcfun_linear : linear f. 
+Proof. move => *; exact: linearP. Qed.
+
+End lcfunproperties.

From a319f0887b41d818cf59206a34785e4ec2326103 Mon Sep 17 00:00:00 2001
From: mkerjean <marie.kerjean@lipn.univ-paris13.fr>
Date: Mon, 30 Mar 2026 22:02:01 +0900
Subject: [PATCH 07/12] doc and changelog

---
 CHANGELOG_UNRELEASED.md          | 25 ++++++++++++++++++++++---
 theories/normedtype_theory/tvs.v |  6 ++++++
 2 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index aaed55eed..3d1293014 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -5,11 +5,30 @@
 ### Added
 
 - in `functions.v`:
-  + mixin ...
+  + Lemma linfunP. linfuneqP, linfun_valP, linfun_rect
+  + Definition linfun_Sub_subproof, linfun_Sub,
+  + HB instance of SubLmodule and pointedType on {linear _->_ | _ }
 
 - in `tvs.v`:
-  + ...
-
+  + HB structure LinearContinuous
+  + HB factory isLinearContinuous
+  + HB instance of linear functions on LinearContinuous and of continuous on LinearContinuous
+  + HB instance of ChoiceType on {linear_continuous _ -> _ }
+  + HB instance of LinearContinuous on the composition of two functions of type LinearContinuous
+  + HB instance of LinearContinuous on the sum of two functions of type LinearContinuous
+  + HB instance of LinearContinuous on the scalar multiplication of a function of type
+    LinearContinuous
+  + HB instance of Continuous on \-f when f is of type LinearContinuous
+  + HB instance of SubModClosed on {linear_continuous _ -> _}
+  + HB instance of SubLModule on  {linear_continuous _ -> _ }
+  + HB instance of LinearContinuous on the null function
+  + Notations {linear_continuous _ -> _ | _ } and {linear_continuous _ -> _ }
+  + Definition lcfun, lcfun_key, lcfun_Sub_suproof, lcfun_Sub, lcfunP
+  + Lemma lcfun_rect, lcfun_valP, lcfun_eqP, null_fun_continuous, lcfun_cvgD,
+    lcfun_continuousD, lcfun_cvgN, lcfun_continuousN, lcfun_cvgZ, lcfunfun_cvgZr,
+    lcfun_continuousM, lcfun_submod_closed
+  + Lemma lcfun_continuous and lcfun_linear
+  
 ### Changed
 
 - moved from `topology_structure.v` to `filter.v`:
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index fc89c61a7..4ca99ec80 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -49,10 +49,16 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a   *)
 (*                             convex tvs from an Lmodule which is also a     *)
 (*                             topological space                              *)
+(* {linear_continuous E -> F} == the type of all linear and continuous        *)
+(*                             functions between E and F, where E is a        *)
+(*                             NbhsLmodule.type and F a NbhsZmodule.type over *)
+(*                             a numDomainType R.                             *)
 (* HB instances:                                                              *)
 (* - The type R^o (R : numFieldType) is endowed with the structure of         *)
 (*   ConvexTvs.                                                               *)
 (* - The product of two Tvs is endowed with the structure of ConvexTvs.       *)
+(* - {linear_continuous E-> F} is endowed with a lmodtType structure when E   *)
+(*    and F are convexTvs.                                                    *)
 (******************************************************************************)
 
 Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"

From 99a1650a789d71ef705d822eac52ff5207abb0ec Mon Sep 17 00:00:00 2001
From: mkerjean <marie.kerjean@lipn.univ-paris13.fr>
Date: Fri, 3 Apr 2026 10:15:50 +0900
Subject: [PATCH 08/12] clean

---
 CHANGELOG_UNRELEASED.md          |  39 +++++----
 classical/functions.v            |  15 ++--
 theories/normedtype_theory/tvs.v | 134 ++++++++++++++++++-------------
 3 files changed, 106 insertions(+), 82 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3d1293014..43ae62430 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -5,29 +5,26 @@
 ### Added
 
 - in `functions.v`:
-  + Lemma linfunP. linfuneqP, linfun_valP, linfun_rect
-  + Definition linfun_Sub_subproof, linfun_Sub,
-  + HB instance of SubLmodule and pointedType on {linear _->_ | _ }
+  + lemmas `linfunP`, `linfuneqP`
+  + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
 
 - in `tvs.v`:
-  + HB structure LinearContinuous
-  + HB factory isLinearContinuous
-  + HB instance of linear functions on LinearContinuous and of continuous on LinearContinuous
-  + HB instance of ChoiceType on {linear_continuous _ -> _ }
-  + HB instance of LinearContinuous on the composition of two functions of type LinearContinuous
-  + HB instance of LinearContinuous on the sum of two functions of type LinearContinuous
-  + HB instance of LinearContinuous on the scalar multiplication of a function of type
-    LinearContinuous
-  + HB instance of Continuous on \-f when f is of type LinearContinuous
-  + HB instance of SubModClosed on {linear_continuous _ -> _}
-  + HB instance of SubLModule on  {linear_continuous _ -> _ }
-  + HB instance of LinearContinuous on the null function
-  + Notations {linear_continuous _ -> _ | _ } and {linear_continuous _ -> _ }
-  + Definition lcfun, lcfun_key, lcfun_Sub_suproof, lcfun_Sub, lcfunP
-  + Lemma lcfun_rect, lcfun_valP, lcfun_eqP, null_fun_continuous, lcfun_cvgD,
-    lcfun_continuousD, lcfun_cvgN, lcfun_continuousN, lcfun_cvgZ, lcfunfun_cvgZr,
-    lcfun_continuousM, lcfun_submod_closed
-  + Lemma lcfun_continuous and lcfun_linear
+  + structure `LinearContinuous`
+  + factory `isLinearContinuous`
+  + instance of `ChoiceType` on `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` with the composition of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the sum of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the scalar multiplication of a function of type
+    `LinearContinuous`
+  + instance of `Continuous` on \-f when f is of type `LinearContinuous`
+  + instance of `SubModClosed` on `{linear_continuous _ -> _}`
+  + instance of `SubLModule` on  `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` on the null function
+  + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }`
+  + definitions `lcfun`, `lcfun_key, `lcfunP`
+  + lemmas `lcfun_eqP`, `null_fun_continuous`, `lcfun_cvgD`,
+   `lcfun_cvgN`, `lcfun_cvgZ`, `lcfunfun_cvgZr`
+  + lemmas `lcfun_continuous` and `lcfun_linear`
   
 ### Changed
 
diff --git a/classical/functions.v b/classical/functions.v
index c68e035f8..bbec34850 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2767,7 +2767,9 @@ Context {K : numDomainType} {E : lmodType K}  {F : lmodType K}
 (**md Beware that `lfun` is reserved for vector types, hence this one has been
  named `linfun` *)
 Definition linfun : {pred E -> F} := mem [set f | linear_for s f ].
+
 Definition linfun_key : pred_key linfun. Proof. exact. Qed.
+
 Canonical linfun_keyed := KeyedPred linfun_key.
 
 End linfun_pred.
@@ -2775,20 +2777,22 @@ End linfun_pred.
 Section linfun.
 Context {R : numDomainType} {E : lmodType R}
   {F : lmodType R} {s : GRing.Scale.law R F}.
+
 Notation T := {linear E -> F | s}.
+
 Notation linfun := (@linfun _ E F s).
 
 Section Sub.
 Context (f : E -> F) (fP : f \in linfun).
 
-Definition linfun_Sub_subproof :=
+#[local] Definition linfun_Sub_subproof :=
   @GRing.isLinear.Build _ E F s f (set_mem fP).
 
 #[local] HB.instance Definition _ := linfun_Sub_subproof.
 Definition linfun_Sub : {linear _  -> _ | _ } := f.
 End Sub.
 
-Lemma linfun_rect (K : T -> Type) :
+Let linfun_rect (K : T -> Type) :
   (forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u.
 Proof.
 move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
@@ -2801,7 +2805,7 @@ congr (GRing.Linear.Pack (GRing.Linear.Class _ _)).
 - by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance.
 Qed.
 
-Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
+Let linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
 Proof. by []. Qed.
 
 HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
@@ -2825,10 +2829,9 @@ End linfun.
 
 Section linfun_lmodtype.
 Context {R : numFieldType} {E F : lmodType R}.
-
 Import GRing.Theory.
 
-Lemma linfun_submod_closed  : submod_closed (@linfun R E F *:%R).
+Let linfun_submod_closed  : submod_closed (@linfun R E F *:%R).
 Proof.
 split; first by rewrite inE; exact/linearP.
 move=> r /= _ _ /linfunP[f] /linfunP[g].
@@ -2843,6 +2846,6 @@ HB.instance Definition _ :=
 
 End linfun_lmodtype.
 
-(* TODO: we wanted to declare this instance in classical_sets.v but failed and did not understand why, also we couldn't generaliz *)
+(* TODO: we wanted to declare this instance in classical_sets.v but failed and did not understand why, also we couldn't generalize *)
 HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
   isPointed.Build {linear E -> F} (\0)%R.
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 4ca99ec80..eda6df758 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -99,6 +99,25 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M
 HB.structure Definition TopologicalNmodule :=
   {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}.
 
+
+Section TopologicalNmodule_theory.
+
+Variable (E : topologicalType) (F : TopologicalNmodule.type).
+(** NB : cvgD in pseudometric_normedZmodule could be lowered to some common
+  structure to convexTvsType and pseudometric, then `lcfun_cvgD` doesn't need to
+  exist anymore (we are however not sure that this deserves the introduction of
+  a new structure that combines nbhs and normedZmodule) *)
+
+Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} (f g : E -> F) a b :
+  f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
+Proof.
+move=> fa ga.
+by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..].
+Qed.
+
+End TopologicalNmodule_theory.
+
+
 HB.mixin Record TopologicalNmodule_isTopologicalZmodule M
     & Topological M & GRing.Zmodule M := {
   opp_continuous : continuous (-%R : M -> M) ;
@@ -109,6 +128,23 @@ HB.structure Definition TopologicalZmodule :=
   {M of TopologicalNmodule M & GRing.Zmodule M
         & TopologicalNmodule_isTopologicalZmodule M}.
 
+Section TopologicalZmoduleTheory.
+Variables (M : topologicalZmodType).
+
+Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2).
+Proof.
+move=> x; apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2))
+  (fun x : M * M => x.1 + x.2)); last exact: add_continuous.
+apply: cvg_pair; first exact: cvg_fst.
+by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous].
+Qed.
+
+Lemma lcfun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U} (f : M -> F) a :
+  f @ U --> a -> \- f @ U --> - a.
+Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
+
+End TopologicalZmoduleTheory.
+
 HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M
     & Topological M & GRing.Zmodule M := {
   sub_continuous : continuous (fun x : M * M => x.1 - x.2) ;
@@ -116,7 +152,7 @@ HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M
 
 HB.builders Context M & PreTopologicalNmodule_isTopologicalZmodule M.
 
-Lemma opp_continuous : continuous (-%R : M -> M).
+Let opp_continuous : continuous (-%R : M -> M).
 Proof.
 move=> x; rewrite /continuous_at.
 rewrite -(@eq_cvg _ _ _ (fun x => 0 - x)); first by move=> y; exact: add0r.
@@ -126,7 +162,7 @@ apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2)).
 exact: sub_continuous.
 Qed.
 
-Lemma add_continuous : continuous (fun x : M * M => x.1 + x.2).
+Let add_continuous : continuous (fun x : M * M => x.1 + x.2).
 Proof.
 move=> x; rewrite /continuous_at.
 rewrite -(@eq_cvg _ _ _ (fun x => x.1 - (- x.2))).
@@ -146,19 +182,6 @@ HB.instance Definition _ :=
 
 HB.end.
 
-Section TopologicalZmoduleTheory.
-Variables (M : topologicalZmodType).
-
-Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2).
-Proof.
-move=> x; apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2))
-  (fun x : M * M => x.1 + x.2)); last exact: add_continuous.
-apply: cvg_pair; first exact: cvg_fst.
-by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous].
-Qed.
-
-End TopologicalZmoduleTheory.
-
 #[short(type="preTopologicalLmodType")]
 HB.structure Definition PreTopologicalLmodule (K : numDomainType) :=
   {M of Topological M & GRing.Lmodule K M}.
@@ -173,6 +196,25 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) :=
   {M of TopologicalZmodule M & GRing.Lmodule K M
         & TopologicalZmodule_isTopologicalLmodule K M}.
 
+Section TopologicalLmodule_theory.
+  
+Variables (R : numFieldType) (E : topologicalType) (F: topologicalLmodType R).
+  
+Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F) (r : R) a :
+  l @ U --> r -> f @ U --> a ->
+  l x *: f x @[x --> U] --> r *: a.
+Proof.
+by move=> *; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
+Qed.
+
+Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a :
+  f @ U --> a -> k \*: f @ U --> k *: a.
+Proof. by apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
+
+
+End TopologicalLmodule_theory.
+
+
 HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M
     & Topological M & GRing.Lmodule R M := {
   scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ;
@@ -180,7 +222,7 @@ HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M
 
 HB.builders Context R M & TopologicalNmodule_isTopologicalLmodule R M.
 
-Lemma opp_continuous : continuous (-%R : M -> M).
+Let opp_continuous : continuous (-%R : M -> M).
 Proof.
 move=> x; rewrite /continuous_at.
 rewrite -(@eq_cvg _ _ _ (fun x => -1 *: x)); first by move=> y; rewrite scaleN1r.
@@ -637,8 +679,11 @@ HB.end.
 
 Section lcfun_pred.
 Context  {K : numDomainType} {E : NbhsLmodule.type K}  {F : NbhsZmodule.type} {s : K -> F -> F}.
+  
 Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ].
+
 Definition lcfun_key : pred_key lcfun. Proof. exact. Qed.
+
 Canonical lcfun_keyed := KeyedPred lcfun_key.
 
 End lcfun_pred.
@@ -651,19 +696,24 @@ Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type
 Section lcfun.
 Context {R : numDomainType} {E : NbhsLmodule.type R}
   {F : NbhsZmodule.type} {s : GRing.Scale.law R F}.
+
 Notation T := {linear_continuous E -> F | s}.
+
 Notation lcfun := (@lcfun _ E F s).
 
 Section Sub.
 Context (f : E -> F) (fP : f \in lcfun).
 
-Definition lcfun_Sub_subproof :=
+#[local] Definition lcfun_Sub_subproof :=
   @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)).
+
 #[local] HB.instance Definition _ := lcfun_Sub_subproof.
+
 Definition lcfun_Sub : {linear_continuous _  -> _ | _ } := f.
+
 End Sub.
 
-Lemma lcfun_rect (K : T -> Type) :
+Let lcfun_rect (K : T -> Type) :
   (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u.
 Proof.
 move=> Ksub [f [[Pf1] [Pf2] [Pf3]]].
@@ -678,7 +728,7 @@ congr (LinearContinuous.Pack (LinearContinuous.Class _ _ _)).
 - by congr isContinuous.Axioms_; exact: Prop_irrelevance.
 Qed.
 
-Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
+Let lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
 Proof. by []. Qed.
 
 HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP.
@@ -724,63 +774,35 @@ Implicit Types (r : R) (f g : {linear_continuous E -> F}).
 Import GRing.Theory.
 
 Lemma null_fun_continuous : continuous (\0 : E -> F).
-Proof.
-by apply: cst_continuous.
-Qed.
+Proof. by apply: cst_continuous. Qed.
 
 HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
 
-(** NB : cvgD in pseudometric_normedZmodule could be lowered to some common
-  structure to convexTvsType and pseudometric, then `lcfun_cvgD` doesn't need to
-  exist anymore (we are however not sure that this deserves the introduction of
-  a new structure that combines nbhs and normedZmodule) *)
-Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
-  f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
-Proof.
-move=> fa ga.
-by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..].
-Qed.
-
-Lemma lcfun_continuousD f g : continuous (f \+ g).
+Let lcfun_continuousD f g : continuous (f \+ g).
 Proof. by move=> /= x; apply: lcfun_cvgD; exact: cts_fun. Qed.
 
-Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a :
-  f @ U --> a -> \- f @ U --> - a.
-Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
-
-Lemma lcfun_continuousN f : continuous (\- f).
-Proof. by move=> /= x; apply: lcfun_cvgN; exact: cts_fun. Qed.
-
 HB.instance Definition _ f g :=
   isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
 
-Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a :
-  l @ U  --> r -> f @ U --> a ->
-  l x *: f x @[x --> U] --> r *: a.
-Proof.
-by move=> *; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
-Qed.
+Let lcfun_continuousN f : continuous (\- f).
+Proof. by move=> /= x; apply: lcfun_cvgN; exact: cts_fun. Qed.
 
-Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a :
-  f @ U --> a -> k \*: f @ U --> k *: a.
-Proof. by apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
+HB.instance Definition _ f :=
+  isContinuous.Build E F (\- f) (@lcfun_continuousN f).
 
-Lemma lcfun_continuousM r g : continuous (r \*: g).
+Let lcfun_continuousM r g : continuous (r \*: g).
 Proof. by move=> /= x; apply: lcfun_cvgZr; exact: cts_fun. Qed.
 
 HB.instance Definition _ r g :=
   isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g).
 
-Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R).
+Let 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].
 by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD].
 Qed.
 
-HB.instance Definition _ f :=
-  isContinuous.Build E F (\- f) (@lcfun_continuousN f).
-
 HB.instance Definition _ :=
   @GRing.isSubmodClosed.Build _  _ lcfun lcfun_submod_closed.
 
@@ -793,9 +815,11 @@ Section lcfunproperties.
 Context {R : numDomainType} {E F : NbhsLmodule.type R}
   (f : {linear_continuous E -> F}).
 
+#[warn="This lemma is here to facilitate discoverability using the `Search` command. Consider using `cts_fun` instead."] 
 Lemma lcfun_continuous : continuous f. 
 Proof. exact: cts_fun. Qed.
 
+#[warn="This lemma is here to facilitate discoverability using the `Search` command. Consider using `linearP` instead"]
 Lemma lcfun_linear : linear f. 
 Proof. move => *; exact: linearP. Qed.
 

From 8bb30dc4ea870c8338c0e9378085025631f16dc3 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 3 Apr 2026 10:32:44 +0900
Subject: [PATCH 09/12] wip

---
 classical/functions.v            | 13 ++++++++++---
 theories/normedtype_theory/tvs.v |  3 ++-
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/classical/functions.v b/classical/functions.v
index bbec34850..df7b1979e 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -129,8 +129,15 @@ Add Search Blacklist "_mixin_".
 (* ```                                                                        *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*Section linfun_lmodtype == canonical lmodtype structure on linear maps      *)
-(*                           between lmodtypes.                               *)
+(*           linfun E F s == membership predicate for linear functions of     *)
+(*                           type E -> F with scalar operator                 *)
+(*                           s : K -> F -> F                                  *)
+(*                           E and F have type lmodType K.                    *)
+(*                           This is used in particular to attach a type of   *)
+(*                           lmodType to {linear E -> F | s}.                 *)
+(*          linfun_spec f == specification for membership of the linear       *)
+(*                           function f                                       *)
+(* ```                                                                        *)
 (*                                                                            *)
 (*                                                                            *)
 (*                                                                            *)
@@ -2816,7 +2823,7 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
 HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
 
 Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
-  | Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
+| Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
 
 Lemma linfunP (f : E -> F) : f \in linfun -> linfun_spec f f (f \in linfun).
 Proof.
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index eda6df758..83e209853 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -52,7 +52,8 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (* {linear_continuous E -> F} == the type of all linear and continuous        *)
 (*                             functions between E and F, where E is a        *)
 (*                             NbhsLmodule.type and F a NbhsZmodule.type over *)
-(*                             a numDomainType R.                             *)
+(*                             a numDomainType R                              *)
+(* ```                                                                        *)
 (* HB instances:                                                              *)
 (* - The type R^o (R : numFieldType) is endowed with the structure of         *)
 (*   ConvexTvs.                                                               *)

From dde18d5e6caa42741441379a0fe8f5e4f11f0ce2 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 3 Apr 2026 11:01:14 +0900
Subject: [PATCH 10/12] check

---
 CHANGELOG_UNRELEASED.md          | 18 +++----
 theories/normedtype_theory/tvs.v | 84 +++++++++++++++++---------------
 2 files changed, 55 insertions(+), 47 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 43ae62430..865949ad3 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -22,8 +22,8 @@
   + instance of `LinearContinuous` on the null function
   + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }`
   + definitions `lcfun`, `lcfun_key, `lcfunP`
-  + lemmas `lcfun_eqP`, `null_fun_continuous`, `lcfun_cvgD`,
-   `lcfun_cvgN`, `lcfun_cvgZ`, `lcfunfun_cvgZr`
+  + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`,
+   `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr`
   + lemmas `lcfun_continuous` and `lcfun_linear`
   
 ### Changed
@@ -35,15 +35,15 @@
 
 - in `tvs.v`:
   + definition `tvsType` -> `convexTvsType`
-  + HB class `Tvs` -> `ConvexTvs`
-  + HB mixin `Uniform_isTvs` -> `Uniform_isConvexTvs`
-  + HB factory `PreTopologicalLmod_isTvs` -> `PreTopologicalLmod_isConvexTvs`
-  + Section `Tvs_numDomain` -> `ConvexTvs_numDomain`
-  + Section `Tvs_numField` -> `ConvexTvs_numField`
-  + Section `prod_Tvs` -> `prod_ConvexTvs`
+  + class `Tvs` -> `ConvexTvs`
+  + mixin `Uniform_isTvs` -> `Uniform_isConvexTvs`
+  + factory `PreTopologicalLmod_isTvs` -> `PreTopologicalLmod_isConvexTvs`
+  + section `Tvs_numDomain` -> `ConvexTvs_numDomain`
+  + section `Tvs_numField` -> `ConvexTvs_numField`
+  + section `prod_Tvs` -> `prod_ConvexTvs`
 
 - in `normed_module.v`
-  + HB mixin ` PseudoMetricNormedZmod_Tvs_isNormedModule` ->
+  + mixin ` PseudoMetricNormedZmod_Tvs_isNormedModule` ->
     ` PseudoMetricNormedZmod_ConvexTvs_isNormedModule`
 
 ### Generalized
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 83e209853..7637b6fa0 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) 2017 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.
@@ -53,6 +53,18 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (*                             functions between E and F, where E is a        *)
 (*                             NbhsLmodule.type and F a NbhsZmodule.type over *)
 (*                             a numDomainType R                              *)
+(*                             The HB class is called LinearContinuous.       *)
+(*                             The notation {linear_continuous E -> F | s}    *)
+(*                             also exists.                                   *)
+(*              lcfun E F s == membership predicate for linear continuous     *)
+(*                             functions of type E -> F with scalar operator  *)
+(*                             s : K -> F -> F                                *)
+(*                             E and F have type convexTvsType K.             *)
+(*                             This is used in particular to attach a type of *)
+(*                             lmodType to {linear_continuous E -> F | s}.    *)
+(*             lcfun_spec f == specification for membership of the linear     *)
+(*                             continuous function f                          *)
+
 (* ```                                                                        *)
 (* HB instances:                                                              *)
 (* - The type R^o (R : numFieldType) is endowed with the structure of         *)
@@ -67,7 +79,7 @@ Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
    format "{ 'linear_continuous'  U  ->  V  |  s }").
 Reserved Notation "'{' 'linear_continuous' U '->' V '}'"
   (at level 0, U at level 98, V at level 99,
-    format "{ 'linear_continuous'  U  ->  V }"). 
+    format "{ 'linear_continuous'  U  ->  V }").
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
@@ -100,16 +112,14 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M
 HB.structure Definition TopologicalNmodule :=
   {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}.
 
-
 Section TopologicalNmodule_theory.
-
 Variable (E : topologicalType) (F : TopologicalNmodule.type).
+
 (** NB : cvgD in pseudometric_normedZmodule could be lowered to some common
-  structure to convexTvsType and pseudometric, then `lcfun_cvgD` doesn't need to
-  exist anymore (we are however not sure that this deserves the introduction of
+  structure to topologicalNmodule and pseudometric, then `fun_cvgD` doesn't need
+  to exist anymore (we are however not sure that this deserves the introduction of
   a new structure that combines nbhs and normedZmodule) *)
-
-Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} (f g : E -> F) a b :
+Lemma fun_cvgD (U : set_system E) {FF : Filter U} (f g : E -> F) a b :
   f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
 Proof.
 move=> fa ga.
@@ -118,7 +128,6 @@ Qed.
 
 End TopologicalNmodule_theory.
 
-
 HB.mixin Record TopologicalNmodule_isTopologicalZmodule M
     & Topological M & GRing.Zmodule M := {
   opp_continuous : continuous (-%R : M -> M) ;
@@ -140,7 +149,8 @@ apply: cvg_pair; first exact: cvg_fst.
 by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous].
 Qed.
 
-Lemma lcfun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U} (f : M -> F) a :
+Lemma fun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U}
+    (f : M -> F) a :
   f @ U --> a -> \- f @ U --> - a.
 Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
 
@@ -198,24 +208,22 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) :=
         & TopologicalZmodule_isTopologicalLmodule K M}.
 
 Section TopologicalLmodule_theory.
-  
-Variables (R : numFieldType) (E : topologicalType) (F: topologicalLmodType R).
-  
-Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F) (r : R) a :
+Variables (R : numFieldType) (E : topologicalType) (F : topologicalLmodType R).
+
+Lemma fun_cvgZ (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F)
+    (r : R) a :
   l @ U --> r -> f @ U --> a ->
   l x *: f x @[x --> U] --> r *: a.
 Proof.
 by move=> *; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
 Qed.
 
-Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a :
+Lemma fun_cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a :
   f @ U --> a -> k \*: f @ U --> k *: a.
-Proof. by apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
-
+Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed.
 
 End TopologicalLmodule_theory.
 
-
 HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M
     & Topological M & GRing.Lmodule R M := {
   scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ;
@@ -679,9 +687,11 @@ HB.instance Definition _ := isContinuous.Build E F f continuousP.
 HB.end.
 
 Section lcfun_pred.
-Context  {K : numDomainType} {E : NbhsLmodule.type K}  {F : NbhsZmodule.type} {s : K -> F -> F}.
-  
-Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ].
+Context  {K : numDomainType} {E : NbhsLmodule.type K}  {F : NbhsZmodule.type}
+  {s : K -> F -> F}.
+
+Definition lcfun : {pred E -> F} :=
+  mem [set f | linear_for s f /\ continuous f ].
 
 Definition lcfun_key : pred_key lcfun. Proof. exact. Qed.
 
@@ -689,10 +699,10 @@ Canonical lcfun_keyed := KeyedPred lcfun_key.
 
 End lcfun_pred.
 
-Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s)
-  : type_scope.
-Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
-  : type_scope.
+Notation "{ 'linear_continuous' U -> V | s }" :=
+  (@LinearContinuous.type _ U%type V%type s) : type_scope.
+Notation "{ 'linear_continuous' U -> V }" :=
+  {linear_continuous U%type -> V%type | *:%R} : type_scope.
 
 Section lcfun.
 Context {R : numDomainType} {E : NbhsLmodule.type R}
@@ -734,13 +744,13 @@ Proof. by []. Qed.
 
 HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP.
 
-Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g.
-Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+Lemma lcfun_eqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; exact/val_inj/funext. Qed.
 
 HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:].
 
 Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
-  | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
+| Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
 
 Lemma lcfunP (f : E -> F) : f \in lcfun -> lcfun_spec f f (f \in lcfun).
 Proof.
@@ -752,7 +762,6 @@ Qed.
 End lcfun.
 
 Section lcfun_comp.
-
 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}).
@@ -769,30 +778,29 @@ HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
 End lcfun_comp.
 
 Section lcfun_lmodtype.
+Import GRing.Theory.
 Context {R : numFieldType} {E F : convexTvsType R}.
 Implicit Types (r : R) (f g : {linear_continuous E -> F}).
 
-Import GRing.Theory.
-
 Lemma null_fun_continuous : continuous (\0 : E -> F).
 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: lcfun_cvgD; exact: cts_fun. Qed.
+Proof. by move=> /= x; apply: fun_cvgD; exact: cts_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: lcfun_cvgN; exact: cts_fun. Qed.
+Proof. by move=> /= x; apply: fun_cvgN; exact: cts_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: lcfun_cvgZr; exact: cts_fun. Qed.
+Proof. by move=> /= x; apply: fun_cvgZr; exact: cts_fun. Qed.
 
 HB.instance Definition _ r g :=
   isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g).
@@ -816,12 +824,12 @@ Section lcfunproperties.
 Context {R : numDomainType} {E F : NbhsLmodule.type R}
   (f : {linear_continuous E -> F}).
 
-#[warn="This lemma is here to facilitate discoverability using the `Search` command. Consider using `cts_fun` instead."] 
-Lemma lcfun_continuous : continuous f. 
+#[warn(note="Consider using `cts_fun` instead.",cats="discoverability")]
+Lemma lcfun_continuous : continuous f.
 Proof. exact: cts_fun. Qed.
 
-#[warn="This lemma is here to facilitate discoverability using the `Search` command. Consider using `linearP` instead"]
-Lemma lcfun_linear : linear f. 
+#[warn(note="Consider using `linearP` instead.",cats="discoverability")]
+Lemma lcfun_linear : linear f.
 Proof. move => *; exact: linearP. Qed.
 
 End lcfunproperties.

From d262b5a44a025f4a88b666b598323b3547c9e057 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 3 Apr 2026 11:07:37 +0900
Subject: [PATCH 11/12] fix

---
 CHANGELOG_UNRELEASED.md | 2 +-
 classical/functions.v   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 865949ad3..84d092744 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -5,7 +5,7 @@
 ### Added
 
 - in `functions.v`:
-  + lemmas `linfunP`, `linfuneqP`
+  + lemmas `linfunP`, `linfun_eqP`
   + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
 
 - in `tvs.v`:
diff --git a/classical/functions.v b/classical/functions.v
index df7b1979e..1290277ae 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2817,8 +2817,8 @@ Proof. by []. Qed.
 
 HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
 
-Lemma linfuneqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
-Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+Lemma linfun_eqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; exact/val_inj/funext. Qed.
 
 HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
 

From ca043ba7787b2c423866887b5e20ee3c7dc1f2ac Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 3 Apr 2026 11:25:40 +0900
Subject: [PATCH 12/12] fix

---
 theories/normedtype_theory/tvs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 7637b6fa0..0acefd866 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -679,7 +679,7 @@ HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.typ
     continuousP : continuous f
   }.
 
-HB.builders Context K E F s f of @isLinearContinuous K E F s f.
+HB.builders Context K E F s f & @isLinearContinuous K E F s f.
 
 HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP.
 HB.instance Definition _ := isContinuous.Build E F f continuousP.