substructures tentative

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -356,7 +356,7 @@ by case: z {zmax} gP => [c [_ _ bp _]] /= gP => x; apply: bp; apply/gP.
 Qed.
 
 End HahnBanach.
-
+ 
 Section Substructures.
 Context (R: numFieldType) (V : normedModType R).
 Variable (A : pred V) (A': subLmodType A).
@@ -368,8 +368,32 @@ Check {linear_continuous (subspace A) -> R^o}.
 
 Check ((subspace A : normedModType R)).
 
+
+(* defined subtvs as (val continuous is not enough *)
+(* Use factory Lmod_isNormed to define subnormed on a subLmodtype *)
+(* define factory subtvs -> subnormed *)
+
 End Substructures.
 
+(*
+HB.mixin Record isSubConvexTvs
+  (R : numDomainType) (E : convexTvsType R) (A : pred E) B &  SubType E A B & GRing.SubLmodule R E B  := {
+  openB : set_system E ;
+  open_includedB : forall b, openB b -> b `<=` A ;  
+  open_restricted: forall b, open b <-> (exists (C : set E) , open C /\ b = A `&` C)
+}.
+
+
+(* Make a factory with subspace *)
+
+(* Will probably need to define every intermediate topological and algebraic structure, see the beginning of tvs.v *)
+
+#[short(type="subConvextvsType")]
+HB.structure Definition SubConvextvsType (R : numDomainType) (V : lmodType R) (S : pred V) :=
+  { W of SubZmodule V S W &
+      Nmodule_isLSemiModule R W & isSubLSemiModule R V S W}.
+*)
+
 
 Section HBGeom.