clean

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -186,20 +186,19 @@ Hypothesis gP : forall z, zornS g z -> z = g.
 
 (*The next lemma proves that when z is of zorn_type, it can be extended on any
 real line directed by an arbitrary vector v *)
-
 
- Lemma domain_extend  (z : zorn_type) v :
+Lemma domain_extend  (z : zorn_type) v :
      exists2 ze : zorn_type, (zornS z ze) & (exists r, (carrier ze)  v r).
- Proof.
- case: (lem (exists r, (carrier z v r))).
-   by case=> r rP; exists z => //; exists r.
- case: z => [c [fs1 ls1 ms1 ps1]] /= nzv.
- have c00 : c 0 0.
-   have <- : phi 0 = 0 by rewrite linear0.
-   by move: ps1; rewrite /extend_graph /= => /(_ 0) /=; rewrite GRing.val0; apply. 
- have [a aP] : exists a,  forall (x : V) (r lambda : R), c x r -> r + lambda * a <= p (x + lambda *: v).
-   suff [a aP] : exists a,  forall (x : V) (r lambda : R), c x r -> 0 < lambda ->
-       r + lambda * a <= p (x + lambda *: v) /\ r - lambda * a <= p (x - lambda *: v).
+Proof.
+case: (lem (exists r, (carrier z v r))).
+  by case=> r rP; exists z => //; exists r.
+case: z => [c [fs1 ls1 ms1 ps1]] /= nzv.
+have c00 : c 0 0.
+  have <- : phi 0 = 0 by rewrite linear0.
+  by move: ps1; rewrite /extend_graph /= => /(_ 0) /=; rewrite GRing.val0; apply. 
+have [a aP] : exists a,  forall (x : V) (r lambda : R), c x r -> r + lambda * a <= p (x + lambda *: v).
+  suff [a aP] : exists a,  forall (x : V) (r lambda : R), c x r -> 0 < lambda ->
+    r + lambda * a <= p (x + lambda *: v) /\ r - lambda * a <= p (x - lambda *: v).
      exists a=> x r lambda cxr.
      have {aP} aP := aP _ _ _ cxr.
      case: (ltrgt0P lambda) ; [by case/aP | move=> ltl0 | move->]; last first.
@@ -356,62 +355,23 @@ 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).
-
-HB.instance Definition _ := NormedModule.on (subspace A).
-
-Check {linear_continuous (subspace A) -> R^o}.
-(* NB : I'm afraid this describes a function continuous on A but linear on the whole V *)
-
-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.
-(*TODO : define on convextvstype once lemmas as continuous_linear_bounded are
-lowered to convextvs *)
+(*TODO : define on convextvstype once issue #1927 solved*)
+  
 Variable (R : realType) (V : normedModType R) (F : pred V)
 (F' : subLmodType F) (f : {linear F' -> R}).
 
 (* once subnormedspaces are correctly defined replace by
 Variable (R : realType) (V : normedModType R) (F : pred V)
-(f : {linear_continuous (subspace F) -> R}).
+(f : {linear_continuous F' -> R}).
 *)
 
-
 Let setF := [set x : V  | exists (z : F'), val z = x].
 
 Theorem HB_geom_normed :
   (exists  r , (r > 0 ) /\ (forall (z : F'), (`|f z| ) <=  `|(val z)| * r)) -> 
-(* hypothesis to delete once this is rebased over linear_continuous
+(* hypothesis to delete once f is of type {linear_continuous _ -> _ }
   and obtain through continuous_linear_bounded  *)
   exists g: {linear_continuous V -> R}, (forall x, (g (val x) = f x)).
 Proof.