mv tvs to normedtype_theory

Author: affeldt-aist

_CoqProject

@@ -75,12 +75,12 @@ theories/homotopy_theory/continuous_path.v
 
 theories/ess_sup_inf.v
 theories/cantor.v
-theories/tvs.v
 
 theories/normedtype_theory/num_normedtype.v
 theories/normedtype_theory/matrix_normedtype.v
 theories/normedtype_theory/ereal_normedtype.v
 theories/normedtype_theory/pseudometric_normed_Zmodule.v
+theories/normedtype_theory/tvs.v
 theories/normedtype_theory/normed_module.v
 theories/normedtype_theory/complete_normed_module.v
 theories/normedtype_theory/urysohn.v

theories/Make

@@ -41,12 +41,12 @@ homotopy_theory/continuous_path.v
 
 ess_sup_inf.v
 cantor.v
-tvs.v
 
 normedtype_theory/num_normedtype.v
 normedtype_theory/matrix_normedtype.v
 normedtype_theory/ereal_normedtype.v
 normedtype_theory/pseudometric_normed_Zmodule.v
+normedtype_theory/tvs.v
 normedtype_theory/normed_module.v
 normedtype_theory/complete_normed_module.v
 normedtype_theory/urysohn.v

theories/normedtype_theory/normedtype.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Export num_normedtype.
-From mathcomp Require Export ereal_normedtype.
 From mathcomp Require Export pseudometric_normed_Zmodule.
+From mathcomp Require Export ereal_normedtype.
 From mathcomp Require Export normed_module.
 From mathcomp Require Export matrix_normedtype.
 From mathcomp Require Export complete_normed_module.

theories/normedtype_theory/num_normedtype.v

@@ -5,7 +5,7 @@ From mathcomp Require Import interval interval_inference archimedean rat.
 From mathcomp Require Import unstable.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality set_interval reals real_interval.
-From mathcomp Require Import topology prodnormedzmodule tvs.
+From mathcomp Require Import topology prodnormedzmodule.
 
 (**md**************************************************************************)
 (* # Preliminaries for norm-related notions                                   *)

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
 From mathcomp Require Import interval interval_inference archimedean.
 From mathcomp Require Import boolp classical_sets functions cardinality.
 From mathcomp Require Import set_interval ereal reals topology.
-From mathcomp Require Import prodnormedzmodule tvs num_normedtype.
+From mathcomp Require Import prodnormedzmodule num_normedtype.
 
 (**md**************************************************************************)
 (* # Normed topological abelian groups                                        *)
@@ -124,6 +124,15 @@ Unshelve. all: by end_near. Qed.
 
 End at_left_right_topologicalType.
 
+HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}.
+HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}.
+HB.structure Definition PreTopologicalNmodule :=
+  {M of Topological M & GRing.Nmodule M}.
+HB.structure Definition PreTopologicalZmodule :=
+  {M of Topological M & GRing.Zmodule M}.
+HB.structure Definition PreUniformNmodule := {M of Uniform M & GRing.Nmodule M}.
+HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}.
+
 HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
     & Num.NormedZmodule R T & PseudoPointedMetric R T := {
   pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |)

theories/tvs.v theories/normedtype_theory/tvs.vtheories/tvs.v renamed to theories/normedtype_theory/tvs.v

@@ -3,7 +3,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
 From mathcomp Require Import interval_inference.
 From mathcomp Require Import boolp classical_sets functions cardinality.
-From mathcomp Require Import set_interval reals topology.
+From mathcomp Require Import set_interval reals topology num_normedtype.
+From mathcomp Require Import pseudometric_normed_Zmodule.
 
 (**md**************************************************************************)
 (* # Topological vector spaces                                                *)
@@ -73,14 +74,9 @@ Local Open Scope ring_scope.
 (* HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}. *)
 (* HB.structure Definition FilteredLmodule (K : numDomainType) := *)
 (*   {M of Filtered M M & GRing.Lmodule K M}. *)
-HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}.
-HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}.
 HB.structure Definition NbhsLmodule (K : numDomainType) :=
   {M of Nbhs M & GRing.Lmodule K M}.
 
-HB.structure Definition PreTopologicalNmodule :=
-  {M of Topological M & GRing.Nmodule M}.
-
 HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M
     & PreTopologicalNmodule M := {
   add_continuous : continuous (fun x : M * M => x.1 + x.2) ;
@@ -89,9 +85,6 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M
 HB.structure Definition TopologicalNmodule :=
   {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}.
 
-HB.structure Definition PreTopologicalZmodule :=
-  {M of Topological M & GRing.Zmodule M}.
-
 HB.mixin Record TopologicalNmodule_isTopologicalZmodule M
     & Topological M & GRing.Zmodule M := {
   opp_continuous : continuous (-%R : M -> M) ;
@@ -191,17 +184,13 @@ HB.instance Definition _ :=
 
 HB.end.
 
-HB.structure Definition PreUniformNmodule := {M of Uniform M & GRing.Nmodule M}.
-
 HB.mixin Record PreUniformNmodule_isUniformNmodule M & PreUniformNmodule M := {
   add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2)
 }.
 
 HB.structure Definition UniformNmodule :=
   {M of PreUniformNmodule M & PreUniformNmodule_isUniformNmodule M}.
 
-HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}.
-
 HB.mixin Record UniformNmodule_isUniformZmodule M
     & Uniform M & GRing.Zmodule M := {
   opp_unif_continuous : unif_continuous (-%R : M -> M)