renamed ConvexTvs

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: mkerjean

CHANGELOG_UNRELEASED.md

@@ -8,6 +8,21 @@
 
 ### Renamed
 
+- 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`
+
+
+- in `normed_module.v`
+  + HB mixin ` PseudoMetricNormedZmod_Tvs_isNormedModule` ->
+    ` PseudoMetricNormedZmod_ConvexTvs_isNormedModule`
+
+
 ### Generalized
 
 ### Deprecated

theories/normedtype_theory/normed_module.v

@@ -76,15 +76,15 @@ Local Open Scope ring_scope.
 
 (** Modules with a norm depending on a numDomain *)
 
-HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V
-    & PseudoMetricNormedZmod K V & Tvs K V := {
+HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V
+    & PseudoMetricNormedZmod K V & ConvexTvs K V := {
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
 #[short(type="normedModType")]
 HB.structure Definition NormedModule (K : numDomainType) :=
-  {T of PseudoMetricNormedZmod K T & Tvs K T
-   & PseudoMetricNormedZmod_Tvs_isNormedModule K T}.
+  {T of PseudoMetricNormedZmod K T & ConvexTvs K T
+   & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}.
 
 HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V
     & PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
@@ -142,9 +142,9 @@ HB.instance Definition _ :=
   PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous.
 HB.instance Definition _ :=
   TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous.
-HB.instance Definition _ := Uniform_isTvs.Build K V locally_convex_set.
+HB.instance Definition _ := Uniform_isConvexTvs.Build K V locally_convex_set.
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ.
+  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ.
 
 HB.end.
 
@@ -154,7 +154,7 @@ Section standard_topology_normedMod.
 Variable R : numFieldType.
 
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Tvs_isNormedModule.Build R R^o (@normrM _).
+  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _).
 
 End standard_topology_normedMod.
 
@@ -1631,7 +1631,7 @@ Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |.
 Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed.
 
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Tvs_isNormedModule.Build K (U * V)%type
+  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K (U * V)%type
   prod_norm_scale.
 
 End prod_NormedModule.

theories/normedtype_theory/tvs.v

@@ -41,17 +41,19 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (*         UniformLmodule K == HB class, join of UniformNmodule and Lmodule   *)
 (*                             with a uniformly continuous scaling operation  *)
 (*                             K is a numFieldType.                           *)
-(*               tvsType R  == interface type for a locally convex            *)
-(*                             tvs on a numDomain R                           *)
-(*                             A tvs is constructed over a uniform space.     *)
-(*                             The HB class is Tvs.                           *)
-(* PreTopologicalLmod_isTvs == factory allowing the construction of a tvs     *)
-(*                             from an Lmodule which is also a topological    *)
-(*                             space                                          *)
+(*         convextvsType R  == interface type for a locally convex            *)
+(*                             tvs on a numDomain R.                          *)
+(*                             A convex tvs is constructed over a uniform     *)
+(*                             space.                                         *)
+(*                             The HB class is ConvexTvs.                     *)
+(* 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 Tvs.    *)
-(* - The product of two Tvs is endowed with the structure of Tvs.             *)
+(* - 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.       *)
 (******************************************************************************)
 
 Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
@@ -306,15 +308,15 @@ HB.instance Definition _ :=
 
 HB.end.
 
-HB.mixin Record Uniform_isTvs (R : numDomainType) E
+HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E
     & Uniform E & GRing.Lmodule R E := {
   locally_convex : exists2 B : set_system E,
     (forall b, b \in B -> convex_set b) & basis B
 }.
 
-#[short(type="tvsType")]
-HB.structure Definition Tvs (R : numDomainType) :=
-  {E of Uniform_isTvs R E & Uniform E & TopologicalLmodule R E}.
+#[short(type="convextvsType")]
+HB.structure Definition ConvexTvs (R : numDomainType) :=
+  {E of Uniform_isConvexTvs R E & Uniform E & TopologicalLmodule R E}.
 
 Section properties_of_topologicalLmodule.
 Context (R : numDomainType) (E : preTopologicalLmodType R) (U : set E).
@@ -352,15 +354,15 @@ Unshelve. all: by end_near. Qed.
 
 End properties_of_topologicalLmodule.
 
-HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E
+HB.factory Record PreTopologicalLmod_isConvexTvs (R : numDomainType) E
     & Topological E & GRing.Lmodule R E := {
   add_continuous : continuous (fun x : E * E => x.1 + x.2) ;
   scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ;
   locally_convex : exists2 B : set_system E,
     (forall b, b \in B -> convex_set b) & basis B
   }.
 
-HB.builders Context R E & PreTopologicalLmod_isTvs R E.
+HB.builders Context R E & PreTopologicalLmod_isConvexTvs R E.
 
 Definition entourage : set_system (E * E) :=
   fun P => exists (U : set E), nbhs (0 : E) U  /\
@@ -449,8 +451,8 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E
     nbhsE.
 HB.end.
 
-Section Tvs_numDomain.
-Context (R : numDomainType) (E : tvsType R) (U : set E).
+Section ConvexTvs_numDomain.
+Context (R : numDomainType) (E : convextvsType R) (U : set E).
 
 Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U).
 Proof. exact/nbhs0N_subproof/scale_continuous. Qed.
@@ -461,11 +463,11 @@ Proof. exact/nbhsT_subproof/add_continuous. Qed.
 Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U).
 Proof. exact/nbhsB_subproof/add_continuous. Qed.
 
-End Tvs_numDomain.
+End ConvexTvs_numDomain.
 
-Section Tvs_numField.
+Section ConvexTvs_numField.
 
-Lemma nbhs0Z (R : numFieldType) (E : tvsType R) (U : set E) (r : R) :
+Lemma nbhs0Z (R : numFieldType) (E : convextvsType R) (U : set E) (r : R) :
   r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ).
 Proof.
 move=> r0 U0; have /= := scale_continuous (r^-1, 0) U.
@@ -474,7 +476,7 @@ near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r.
 by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x].
 Unshelve. all: by end_near. Qed.
 
-Lemma nbhsZ  (R : numFieldType) (E : tvsType R) (U : set E) (r : R) (x :E) :
+Lemma nbhsZ  (R : numFieldType) (E : convextvsType R) (U : set E) (r : R) (x :E) :
   r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ).
 Proof.
 move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U.
@@ -483,7 +485,7 @@ near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r.
 by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z].
 Unshelve. all: by end_near. Qed.
 
-End Tvs_numField.
+End ConvexTvs_numField.
 
 Section standard_topology.
 Variable R : numFieldType.
@@ -537,12 +539,12 @@ HB.instance Definition _ :=
 HB.instance Definition _ :=
   TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous.
 HB.instance Definition _ :=
-  Uniform_isTvs.Build R R^o standard_locally_convex_set.
+  Uniform_isConvexTvs.Build R R^o standard_locally_convex_set.
 
 End standard_topology.
 
-Section prod_Tvs.
-Context (K : numFieldType) (E F : tvsType K).
+Section prod_ConvexTvs.
+Context (K : numFieldType) (E F : convextvsType K).
 
 Local Lemma prod_add_continuous :
   continuous (fun x : (E * F) * (E * F) => x.1 + x.2).
@@ -598,6 +600,6 @@ HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build
 HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build
   K (E * F)%type prod_scale_continuous.
 HB.instance Definition _ :=
-  Uniform_isTvs.Build K (E * F)%type prod_locally_convex.
+  Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex.
 
-End prod_Tvs.
+End prod_ConvexTvs.