subnormed

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -376,20 +376,38 @@ Qed.
 
 End HahnBanach.
 
+Section Substructures.
+Context (R: numFieldType) (V : normedModType R).
+Variable (A : pred V).
+
+HB.instance Definition _ := NormedModule.on (subspace A).
+
+Check {linear_continuous (subspace A) -> R^o}.
+
+End Substructures.
+
 Section HBGeom.
+(*Variable (R : realType) (V : normedModType R) (F : pred V)
+(F' : subLmodType F) (f : {linear F' -> R}).*)
+
 Variable (R : realType) (V : normedModType R) (F : pred V)
-(F' : subLmodType F) (f : {linear F' -> R}).
+(f : {linear_continuous (subspace F) -> R}).
+
+
+(*Let setF := [set x : V  | exists (z : F'), val z = x].*)
 
-Let setF := [set x : V  | exists (z : F'), val z = x].
 
 (* TODO : define (F : subNormedModType V) so as to have (f : {linear_continuous F ->
 R}), and to obtain the first hypothesis of the following theorem through the
 lemmas continuous_linear_bounded*)
+ 
+Check continuous_linear_bounded. 
 
 Theorem HB_geom_normed :
-   (exists  r , (r > 0 ) /\ (forall (z : F'), (`|f z| ) <=  `|(val z)| * r)) ->
-  exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall (x : F'), (g (val x) = f x)).
+  (* (exists  r , (r > 0 ) /\ (forall (z : F'), (`|f z| ) <=  `|(val z)| * r)) ->*)
+  exists g: {linear_continuous V -> R}, (forall x : V, F x -> (g x = f x)).
 Proof.
+  (*apply continuous_linear_bounded*)
   move=> [r [ltr0 fxrx]].
   pose p:= fun x : V => `|x|*r.
  have convp: (@convex_function _ _ [set: V] p).