diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2d85fdc0a..bd7eb6fb4 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -248,6 +248,43 @@
   + definition `preimage_set_system`
   + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
     `preimage_set_system_id`
+- in `functions.v`:
+  + lemmas `linfunP`, `linfun_eqP`
+  + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
+
+- in `tvs.v`:
+  + structure `LinearContinuous`
+  + factory `isLinearContinuous`
+  + instance of `ChoiceType` on `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` with the composition of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the sum of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the scalar multiplication of a function of type
+    `LinearContinuous`
+  + instance of `Continuous` on \-f when f is of type `LinearContinuous`
+  + instance of `SubModClosed` on `{linear_continuous _ -> _}`
+  + instance of `SubLModule` on  `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` on the null function
+  + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }`
+  + definitions `lcfun`, `lcfun_key, `lcfunP`
+  + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`,
+   `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr`
+  + lemmas `lcfun_continuous` and `lcfun_linear`
+  
+  + ...
+- in `derive.v`:
+  + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
+  + lemmas `derivable0`, `derive0`, `is_derive0`
+- in `topology_structure.v`:
+  + lemma `not_limit_pointE`
+
+- in `separation_axioms.v`:
+  + lemmas `limit_point_closed`
+- in `convex.v`:
+  + lemma `convex_setW`
+- in `convex.v`:
+  + lemma `convexW`
+
+### Changed
 
 - moved from `topology_structure.v` to `filter.v`:
   + lemma `continuous_comp` (and generalized)
@@ -354,6 +391,31 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- in set_interval.v
+  + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized)
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+  + structure `SubNormedZmodule`, notation `subNormedZmodType`
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+  
+### Changed
+
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definition `preimage_set_system`
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
+    `preimage_set_system_id`
+
+- moved from `topology_structure.v` to `filter.v`:
+  + lemma `continuous_comp` (and generalized)
+
+- in `numfun.v`:
+  + `fune_abse` renamed to `funeposDneg` and direction of the equality changed
+  + `funeposneg` renamed to `funeposBneg` and direction of the equality changed
+  + `funeD_posD` renamed to `funeDB` and direction of the equality changed
+
 ### Renamed
 
 - in `tvs.v`:
diff --git a/CHANGELOG_UNRELEASED_new.md b/CHANGELOG_UNRELEASED_new.md
new file mode 100644
index 000000000..49464d2a9
--- /dev/null
+++ b/CHANGELOG_UNRELEASED_new.md
@@ -0,0 +1,52 @@
+# Changelog (unreleased)
+
+## [Unreleased]
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+  + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge)
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+
+- in `filter.v`:
+  + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+
+- in `topology_structure.v`:
+  + structure `SubTopological`, notation `subTopologicalType`
+
+- in `tvs.v`:
+  + structure `SubConvexTvs`, notation `subConvexTvsType`
+
+- in `normed_module.v`:
+  + structure `SubNormedModule`, notation `subNormedModType`
+  + instance `ent_xsection_filter`
+  + factory `SubLmodule_isSubNormedmodule`
+
+- new file `hahn_banach_theorem.v`:
+  + module `LinearGraph`
+    * definitions `graph`, `linear_graph`
+    * lemmas `lingraph_00`, `lingraphZ`, `lingraphD`
+  + module `HahnBanachZorn`
+    * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph`
+    * record `zorn_type`
+    * definition `zphi`
+    * lemma `zorn_type_eq`
+    * definition `zornS`
+    * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
+  + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
+
+### Deprecated
+
+### Renamed
+
+### Generalized
+
+### Removed
+
+
+
+
diff --git a/classical/unstable.v b/classical/unstable.v
index 9d2432a9c..4064fcda6 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -671,7 +671,27 @@ Proof.
 by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD.
 Qed.
 
+Lemma distC (v w : L) : norm (v - w) = norm (w - v).
+Proof.
+by rewrite -(normN (v - w)) opprB.
+Qed.
+
 End Theory.
+
+Section realTheory.
+Variables (K : realDomainType) (L : lmodType K) (norm : SemiNorm.type L).
+
+Lemma seminorm_normrB x y: `|norm x - norm y| <= norm (x - y).
+Proof.
+have [pxy | pyx] := leP (norm x) (norm y).
+  rewrite ler0_norm ?subr_le0 // opprB.
+  rewrite lerBlDl; rewrite  -(@normN _ _ norm (x-y)) opprB.
+  by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK.
+rewrite gtr0_norm ?subr_gt0 // lerBlDl.
+by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK.
+Qed.
+
+End realTheory.
 End Theory.
 
 Module Import Exports. HB.reexport. End Exports.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 1252178b3..5af23c18a 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -132,7 +132,7 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
-Let ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r).
+Lemma ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r).
 Proof.
 apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
 rewrite inE/=.
@@ -145,16 +145,29 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
 by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
+#[local] Lemma ball_balanced_set (r : K) : balanced_set (ball (0 : V) r).
+Proof.
+move => t /= t1 z /= [y].
+rewrite -ball_normE /= !sub0r !normrN => + <-.
+rewrite normrZ.
+case: (eqVneq `|t| (1 : K)).
+  by move=> -> ; rewrite mul1r.
+move=> t11.
+have : (`|t| <1) by rewrite lt_neqAle; apply/andP; split.
+by move => lt1 yr; rewrite -[ltRHS]mul1r ltr_pM ?normr_ge0.
+Qed.
+
 (** NB: we have almost the same proof in `tvs.v` *)
 Let locally_convex_set :
   exists2 B : set_system (convex_lmodType V),
-    (forall b, b \in B -> convex_set b) & basis B.
+    (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B.
 Proof.
-exists [set B | exists (x : convex_lmodType V) r, B = ball x r].
-  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex_set.
-split; first by move=> B [x] [r] ->; exact: ball_open.
-move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
-by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
+exists [set B | exists2 r, 0 < r &  B = ball 0 r].
+  move=> b; rewrite inE /= => -[r _ ->]; split; first by exact: ball_convex_set.
+  by exact: ball_balanced_set.
+split; first by move=> /= a [r r0 ->]; apply: nbhsx_ballx.
+move=> /= b; rewrite -nbhs_ballE => -[r /= r0] b0r /=.
+by exists (ball 0 r)=> //; exists r.
 Qed.
 
 HB.instance Definition _ :=
@@ -2012,10 +2025,6 @@ rewrite (le_lt_trans (fr r _ _))// -?ltr_pdivlMl//.
 by near: z; apply: cvgr_dist_lt => //; rewrite mulrC divr_gt0.
 Unshelve. all: by end_near. Qed.
 
-Lemma continuousfor0_continuous (f : {linear V -> W}) :
-  {for 0, continuous f} -> continuous f.
-Proof. by move=> /continuous_linear_bounded/bounded_linear_continuous. Qed.
-
 Lemma linear_bounded_continuous (f : {linear V -> W}) :
   bounded_near f (nbhs 0) <-> continuous f.
 Proof.
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 41126a781..b1daf833d 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -5,7 +5,7 @@ From mathcomp Require Import interval_inference.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality.
-From mathcomp Require Import convex set_interval reals topology num_normedtype.
+From mathcomp Require Import convex set_interval reals initial_topology topology num_normedtype.
 From mathcomp Require Import pseudometric_normed_Zmodule.
 
 (**md**************************************************************************)
@@ -78,6 +78,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (*   and F are convexTvs.                                                     *)
 (******************************************************************************)
 
+
 Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
   (at level 0, U at level 98, V at level 99,
    format "{ 'linear_continuous'  U  ->  V  |  s }").
@@ -96,6 +97,142 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+
+
+Module DDist.
+Section dDist.
+Context (R: numDomainType) (n : nat).
+
+Record d :=  {
+   t :> n.-tuple R ;
+   le1 : \sum_(a <- t) `|a| <= 1}.
+
+End dDist.
+End DDist.
+Coercion DDist.t : DDist.d >-> tuple_of.
+
+
+Reserved Notation "{ 'ddist' n }" (at level 0, format "{ 'ddist'  n }").
+Reserved Notation "R '.-ddist' n" (at level 2, format "R '.-ddist'  n").
+
+Notation "R '.-ddist' n" := (DDist.d R n%type).
+Notation "{ 'ddist' n }" := (_.-ddist n).
+
+
+Section absolutely_convex.
+Context (K : numDomainType) (V : lmodType K).
+
+Definition balanced_set (A : set V) := forall r, `|r| <= 1 ->  (fun x => r *: x) @`A `<=` A.
+
+Definition absolutely_convex_set  (A : set V) := convex_set A /\ balanced_set A.
+
+Definition absorbing_set (A : set V) := forall x : V, exists a, exists2 r, a \in A & x = r *:a.
+
+Definition pabsorbing_set (A : set V) := forall x : V, exists2 r, 0 < r & r*: x \in A.
+
+Definition absolutely_convex_hull  (A : set V) := smallest absolutely_convex_set A.
+
+(* TODO : move to convex.v *)
+Lemma setI_convex : setI_closed (@convex_set K V).
+Proof.
+move=> A B cA cB x y r /[!inE] -[xA xB] [yA yB]; split; apply/set_mem.
+by apply/cA; apply/mem_set.
+by apply/cB; apply/mem_set.
+Qed.
+
+Lemma bigcap_convex : bigcap_closed (@convex_set K V).
+Proof.
+move=> H Hconv x y r /[!inE] /= Hx Hy A /[dup] HA /Hconv /(_ _ _ _ _ _ )/set_mem; apply.
+- by apply: mem_set; apply: Hx.
+- by apply: mem_set; apply: Hy.
+Qed.
+
+Lemma setI_balanced : setI_closed balanced_set.
+Proof.
+move=> A B bA bB x r /=; rewrite subsetI; split => z /= [t [At Bt] <-].
+- by apply: (bA _ r)  => //; exists t.
+- by apply: (bB _ r)  => //; exists t.
+Qed.
+
+Lemma bigcap_balanced : bigcap_closed balanced_set.
+Proof.
+move=> H Hconv /= r r1; apply: sub_bigcap => A HA x /= [t Ht <-].
+apply: (Hconv A HA r r1) => //.
+by exists t; first by apply: Ht.
+Qed.
+
+Lemma absolutely_convex_hull_set  (A : set V) : absolutely_convex_set (absolutely_convex_hull A).
+Proof.
+apply: bigcap_closed_smallest => H Habs.
+split.
+- by apply: bigcap_convex; apply: (subset_trans Habs); apply: subIsetl.
+- by apply: bigcap_balanced; apply: (subset_trans Habs); apply: subIsetr.
+Qed.
+
+Lemma absolutely_convex_hullE  (A : set V):
+  absolutely_convex_hull A = [set a | exists n  (t: {ddist n}) (l : n.-tuple V),
+                             [set` l] `<=` A  /\  a = \sum_(i < n) t`_i *: l`_i].
+Abort.
+
+Lemma absolutely_convex_hull_subset  (A : set V): A `<=` absolutely_convex_hull A.
+Proof.
+by exact: sub_gen_smallest.
+Qed.
+
+Lemma absolutely_convex0 (B : set V) :  B !=set0 -> absolutely_convex_set B  ->  B 0.
+Proof.
+move => [] x Bx []  _ /(_ 0); rewrite normr0 ler01 // => /(_ isT) /(_ 0); apply.
+by exists x; rewrite //= scale0r.
+Qed.
+
+End absolutely_convex.
+
+
+Notation "A `+ B" := [set x + y | x in A & y in B] (at level 54).
+Notation "r `*: B" := [set r *: x | x  in B] (at level 54).
+
+Section addsetTheory.
+
+Lemma addsubset (E : zmodType) (A B C D: set E):
+  A `<=` B -> C `<=` D -> (A `+ C) `<=` (B `+ D).
+Proof.
+by move=> AB CD z [a /AB Ba [c /CD Dc <-]]; exists a => //; exists c.
+Qed.
+
+Lemma addset0 (E : zmodType) (A: set E):
+ ([set 0] `+ A) = A.
+Proof.
+apply/seteqP; split => z /=.
+  by move=> [+ -> [y]]; rewrite add0r => + + <-.
+by move=> Az; exists 0 => //; exists z; rewrite ?add0r.
+Qed.
+
+Lemma addsetI (E : zmodType) (A B : set E) (x : E) :
+[set x] `+ (A `&` B) = ([set x] `+ A) `&` ([set x] `+ B).
+Proof.
+apply/seteqP; split => z.
+   by move => [r Cr] [y [Ay By] <- {z}]; split => /=; exists r => //; exists y => //.
+move => /= [[r ->] [y Ay] <- {z}] [x' ->] [y' By'].
+move=> /(congr1 (fun h => h - x)).
+rewrite addrAC subrr add0r addrAC subrr add0r => yy'.
+rewrite yy' in By' *.
+by exists x  => //;  exists y' => //; rewrite ?yy'; first by split.
+Qed.
+
+Lemma addsubsetA (E : zmodType) p c (D : set E) :
+  [set p + c] `+ D `<=` [set p] `+ ([set c] `+ D).
+Proof.
+move=> x/= [y ->{y}] [z Dz <-{x}].
+exists p => //.
+exists (c + z) => //.
+  exists c => //.
+  by exists z.
+by rewrite addrA.
+Qed.
+
+End addsetTheory.
+
+
 (* HB.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}. *)
 (* HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}. *)
 (* HB.structure Definition PointedLmodule (K : numDomainType) := *)
@@ -144,6 +281,15 @@ Lemma sum_continuous (I : Type) (r : seq I) (P : pred I) (f : I -> E -> F) :
   continuous (fun x1 : E => \sum_(i <- r | P i) f i x1).
 Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed.
 
+Lemma continuous_shift (x y: F) :
+ {for x, continuous (+%R^~ y)}.
+Proof.
+have -> : +%R^~ y = (fun z => z.1 + z.2) \o (fun z => (z,y)) by apply: funext.
+apply: continuous_comp.
+by apply: cvg_pair => //=; exact: cvg_cst.
+exact: (@add_continuous _ (x,y)).
+Qed.
+
 End TopologicalNmodule_theory.
 
 HB.mixin Record TopologicalNmodule_isTopologicalZmodule M
@@ -157,7 +303,7 @@ HB.structure Definition TopologicalZmodule :=
         & TopologicalNmodule_isTopologicalZmodule M}.
 
 Section TopologicalZmoduleTheory.
-Variables (M : topologicalZmodType).
+Variables (M : topologicalZmodType) (E : topologicalType).
 
 Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2).
 Proof.
@@ -172,6 +318,28 @@ Lemma fun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U}
   f @ U --> a -> \- f @ U --> - a.
 Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
 
+
+Lemma addx_nbhs x (b : set M): nbhs 0 b <-> nbhs x ([set x] `+ b).
+Proof.
+split.
+  rewrite -(subrr x) => /continuous_shift.
+  suff -> : [set x] `+  b = +%R^~ (- x) @^-1` b by [].
+  apply: funext => z /=; apply: propext; split.
+    by move=> [? -> [y By] <-]; rewrite addrAC subrr add0r.
+  by move=> byx; exists x => //; exists (z - x) => //; rewrite addrCA subrr addr0.
+move=> nx.
+suff -> : b =  +%R^~ (x) @^-1` ([set x] `+  b ) by apply: continuous_shift; rewrite add0r.
+apply: funext => z /=; apply: propext; split.
+  by move=> bz; exists x => //; exists z => //; rewrite addrC.
+by move=> [? -> [y By]]; rewrite addrC => /addIr <-.
+Qed.
+
+Lemma subx_nbhs x (b : set M):  nbhs 0 ([set -x] `+ b) <-> nbhs x b.
+Proof.
+have -> : b = [set x ] `+ ([set -x] `+ b). admit.
+split; move/addx_nbhs => /=. admit.
+Abort.
+
 End TopologicalZmoduleTheory.
 
 HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M
@@ -226,7 +394,7 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) :=
         & TopologicalZmodule_isTopologicalLmodule K M}.
 
 Section TopologicalLmodule_theory.
-Variables (R : numFieldType) (E : topologicalType) (F : topologicalLmodType R).
+Variables (R : numFieldType) (E : topologicalType) (F G: topologicalLmodType R).
 
 Lemma fun_cvgZ (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F)
     (r : R) a :
@@ -240,6 +408,31 @@ Lemma fun_cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a :
   f @ U --> a -> k \*: f @ U --> k *: a.
 Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed.
 
+
+(* TODO : look for and factorise similar lemma in normedtype *)
+Lemma continuousfor0_continuous (f : {linear F -> G}) :
+ {for 0, continuous f} -> continuous f.
+Proof.
+move=> cont0 x.
+suff: (f y - f x)@[y --> x] --> (0 : G).
+  have -> : (fun y : F => f y - f x) = (fun y : F => f (y - x) : G).
+    by apply: funext => y; rewrite linearB.
+  move=> fxfy /= A nA /=.
+  pose B := [set z | exists2 y : G, A y & z = y - f x].
+  have /fxfy : nbhs 0 B.
+    have -> : B = (+%R^~ (-( - (f x)))) @^-1` A.
+      rewrite opprK; apply/seteqP; split.
+        by move=> y /= [z] ? ->; rewrite subrK //; exists z.
+      by move=> z /= ?; exists (z + f x)=> //; rewrite addrK.
+    have:= (@continuous_shift  _  (0 : G)  (f x) A).
+    by rewrite opprK add0r => /(_ nA); apply.
+  rewrite /nbhs /=; apply/filterS => z /=; rewrite /B /=.
+  by move => -[y] Ay; rewrite linearD linearN => /(subIr (f x)) ->.
+have -> : (fun y => f y - f x) = (fun y => f(y -x)) by apply: funext => y; rewrite linearB.
+apply: cvg_comp; last by rewrite -(linear0 f); apply: cont0.
+by move => A nA /=;  apply: continuous_shift; rewrite subrr.
+Qed.
+
 End TopologicalLmodule_theory.
 
 HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M
@@ -327,7 +520,7 @@ HB.instance Definition _ :=
 HB.end.
 
 Section UniformZmoduleTheory.
-Variables (M : UniformZmodule.type).
+Variables (M: UniformZmodule.type).
 
 Lemma sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2).
 Proof.
@@ -344,6 +537,8 @@ exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split.
 by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)).
 Qed.
 
+
+
 End UniformZmoduleTheory.
 
 HB.structure Definition PreUniformLmodule (K : numDomainType) :=
@@ -392,7 +587,7 @@ HB.end.
 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
+    (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0)  B
 }.
 
 #[short(type="convexTvsType")]
@@ -462,26 +657,24 @@ HB.instance Definition _ :=
 Local Open Scope convex_scope.
 
 Let locally_convex_sub : exists2 B : set_system sub_init_topo,
-  (forall b, b \in B -> convex_set b) & basis B.
+  (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B.
 Proof.
-have [B convexB [openB/= genB]] := @locally_convex R V.
+have [B absconvB [B0 nbhsb]] := @locally_convex R V.
+rewrite /filter_from /= in nbhsb.
 exists [set a | exists2 b, B b & \val @^-1` b = a].
-  move=> a /[!inE]/= -[b Bb ba] r s l ra sa.
-  suff : \val (r <|l|> s) \in b by rewrite !inE /= -ba.
-  rewrite !GRing.valD !GRing.valZ convexB//; first exact: mem_set.
-  - by move: ra; rewrite -ba !inE.
-  - by move: sa; rewrite -ba !inE.
-split => /=.
-  move=> a/= [b Bb <-]; rewrite /open/= /initial_open/=; exists b => //.
-  exact: openB.
-move=> x a [/= b [[/=c openc] cb bx ba]].
-rewrite /nbhs/= /filter_from/=.
-have : nbhs (val x) c.
- rewrite nbhsE /=; exists c => //; split => //.
- by move: bx; rewrite -cb.
-move/genB => [d [Bd dx dc]].
-exists (\val @^-1` d); first by split => //; exists d.
-by move=> y dy; apply: ba; rewrite -cb; exact: dc.
+  move=> a; rewrite inE /= => -[b] /mem_set/absconvB [convb balb] <-; split.
+    move => r s l ra sa; suff : \val (r <|l|> s) \in b by [].
+    by rewrite !GRing.valD !GRing.valZ convb.
+  move=> /= r r1 x /= [rx] ? <-; apply: balb => /=; first by exact: r1.
+  by exists (\val rx); last by rewrite GRing.valZ.
+split.
+  move=> ? /= [b /B0] + <-.
+  by rewrite -[X in nbhs X _ ->  _](linear0 (\val : U -> V)); exact: initial_nbhs.
+move=> /= A [a' [/= [/= b ob <-] /= b0 ba]].
+have /nbhsb  [b' Bb bb'] : nbhs 0 b.
+  by apply: open_nbhs_nbhs; split; rewrite -?(linear0 (\val : U -> V)).
+exists (val @^-1` b') => /=; last by move => x /= /bb' /ba.
+by exists b'.
 Qed.
 
 Local Close Scope convex_scope.
@@ -508,7 +701,7 @@ Lemma nbhs0N_subproof (f : continuous (fun z : R^o * E => z.1 *: z.2)) :
   nbhs 0 U -> nbhs 0 (-%R @` U).
 Proof. by move => Ux; rewrite -oppr0; exact: nbhsN_subproof. Qed.
 
-Lemma nbhsT_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (x : E) :
+Lemma nbhsD_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (x : E) :
   nbhs 0 U -> nbhs x (+%R x @` U).
 Proof.
 move => U0; have /= := f (x, -x) U; rewrite subrr => /(_ U0).
@@ -533,7 +726,7 @@ HB.factory Record PreTopologicalLmod_isConvexTvs (R : numDomainType) 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
+    (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B
   }.
 
 HB.builders Context R E & PreTopologicalLmod_isConvexTvs R E.
@@ -548,8 +741,8 @@ Proof. exact/nbhs0N_subproof/scale_continuous. Qed.
 Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U).
 Proof. exact/nbhsN_subproof/scale_continuous. Qed.
 
-Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U).
-Proof. exact/nbhsT_subproof/add_continuous. Qed.
+Let nbhsD (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U).
+Proof. exact/nbhsD_subproof/add_continuous. Qed.
 
 Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U).
 Proof. exact/nbhsB_subproof/add_continuous. Qed.
@@ -562,7 +755,7 @@ split; first by exists [set: E]; split; first exact: filter_nbhsT.
   exists (U `&` V); split => [|xy].
     by exists (B `&` C); [exact: open_nbhsI|exact: setISS].
   by rewrite !in_setI => /andP[/Bxy-> /Cxy->].
-by move=> P Q PQ [U [HU Hxy]]; exists U; split=> [|xy /Hxy /[!inE] /PQ].
+by move=> P Q PQ [U [HU Hxy]]; exists U; split => [|xy /Hxy /[!inE] /PQ].
 Qed.
 
 Local Lemma entourage_refl (A : set (E * E)) :
@@ -611,7 +804,7 @@ apply/funext => U; apply/propext => /=; rewrite /entourage /=; split.
   move=> Uxy; exists (v - x); last by rewrite addrC subrK.
   by exists (x - v); rewrite ?opprB.
 - move=> [A [U0 [nU UA]] H]; near=> z; apply: H; apply/xsectionP/set_mem/UA.
-  near: z; rewrite nearE; have := nbhsT x (nbhs0N nU).
+  near: z; rewrite nearE; have := nbhsD x (nbhs0N nU).
   rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U0])//.
   apply/funext => /= z /=; apply/propext; split.
     by move=> [x0] [x1 Ux1 <-] <-; rewrite opprB addrC subrK inE.
@@ -624,7 +817,6 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E
     entourage_inv entourage_split_ex
     nbhsE.
 
-
 HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous.
 
 HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous.
@@ -633,18 +825,346 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex.
 
 HB.end.
 
+
+(* TODO : how to make a mixin isConvexTvssat of the following axioms, as open_at0 has to be redefined each time 
+{
+open_at0 : set_system E;
+mem0_setsystem : forall B, open_at0 B -> B (0 : E);
+split_setsystem : forall B, open_at0 B -> exists2 C, open_at0 C & ( C `+ C  `<=` B);
+expand_setsystem : forall B r, open_at0 B -> (0 <r ) -> exists2 U, open_at0 U & (r `*: U `<=` B);
+convex_setsystem : forall B, open_at0 B -> convex_set B
+}.
+
+HB.structure Definition ConvexTvsat (R : numDomainType) := {E of GRing.Lmodule R E & isConvexTvsat R E}.
+*)
+
+
+HB.factory Record Nbhsbasisat0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E (*& isConvexTvsat R E*) := {
+  nbhsbasis_at0 : set_system E ; (*TODO rename to filterbasis_at0*)
+  nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U;
+  nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V ->
+    exists2 W, nbhsbasis_at0 W & W `<=` U `&` V ;
+  mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0 ;
+  expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> (*0 <= r ->*)
+    exists2 U, nbhsbasis_at0 U & r `*: U `<=` B ; (* implies circled *)
+  absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B;
+  absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B }.
+
+Definition nbhs_frombasis0 (R : numFieldType) (E : zmodType)
+    (nbhsbasis_at0 : set_system E) (x : E) :=
+  filter_from [set U | exists2 V, nbhsbasis_at0 V & [set x] `+ V = U] id.
+(*
+Definition nbhs_fromfilter0  (R: numDomainType) (E : zmodType) (nbhsbasis_at0 : set_system E) (x : E) U :=
+exists2 V, ((filter_from nbhsbasis_at0 id) V) & ([set x] `+ V `<=` U).
+*)
+
+HB.builders Context R E & Nbhsbasisat0_isConvexTvs R E.
+
+Let nbhs_fromfilter0 := @nbhs_frombasis0 R E (nbhsbasis_at0).
+
+Lemma split_nbhsbasisat0 : forall B, nbhsbasis_at0 B ->
+    exists2 C, nbhsbasis_at0 C & C `+ C `<=` B.
+Proof.
+move => B /(@expand_nbhsbasisat0 _ (2)) [U fU UB].
+exists U => //.
+move => /= x [u] Uu [v] Uv <-.
+apply: UB.
+exists (2^-1 *: (u+v)); last by by rewrite scalerA mulfV // scale1r.
+rewrite scalerDr.
+have [convU _] := absconvex_nbhsbasisat0 fU.
+have H : (0 : R) <= 2^-1 by [].
+have G : (2^-1 : R) <= 1 by rewrite invf_le1 ?lerDl //.
+pose r := Itv01 H G.
+have := (convU u v r).
+rewrite !inE => /(_ Uu Uv); rewrite /conv /=.
+suff -> :  (2^-1).~ = 2^-1 :> R by []. (* should be a lemma in convex *)
+apply: (@mulIf _ 2%:R); rewrite /((_).~) //.
+by rewrite mulrBl mulVf // mul1r // addrK.
+Qed.
+
+#[local] Lemma nbhs_filter : forall p : E, ProperFilter (nbhs_fromfilter0 p).
+Proof.
+rewrite /nbhs_fromfilter0 => p.
+apply: filter_from_proper.
+  apply: filter_from_filter => /=.
+  have [U fU] := nonempty_nbhsbasisat0.
+  by exists ([set p] `+ U) => //=; exists U.
+  move=> _ _ /= [U0 FU <-] [V0 FV <-].
+  have [W FW WUV] := nbhsbasis_at0I FU FV.
+  exists ([set p] `+ W); first by exists W.
+  rewrite -addsetI; exact: addsubset.
+move=> _ /= [V FV]  <-.
+by exists p; exists p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0.
+Qed.
+
+#[local] Lemma nbhs_singleton : forall (p : E) (A : set E), nbhs_fromfilter0 p A -> A p.
+Proof.
+move=> p A [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//.
+exact: mem0_nbhsbasisat0.
+Qed.
+
+#[local] Lemma nbhs_nbhs (p : E) (A : set E) : nbhs_fromfilter0 p A ->
+  nbhs_fromfilter0 p (nbhs_fromfilter0^~ A).
+Proof.
+rewrite /nbhs_fromfilter0/=.
+move=> [B/= [C f0C <- pCA]] //=.
+have [D f0D DDC] := split_nbhsbasisat0 f0C.
+exists ([set p] `+ D); first by exists D.
+move=> _ [/= _] -> [c Cc <-] /=.
+exists ([set p + c] `+ D) => //; first by exists D.
+apply: (subset_trans _ pCA).
+apply: (@subset_trans _ ([set p] `+ ([set c] `+ D))); first by exact: addsubsetA.
+apply: addsubset => //; apply: subset_trans DDC; apply: addsubset => //.
+by move=> x ->.
+Qed.
+
+HB.instance Definition _ := @hasNbhs.Build E (nbhs_fromfilter0).
+
+HB.instance Definition _ := @Nbhs_isNbhsTopological.Build E nbhs_filter nbhs_singleton nbhs_nbhs.
+
+
+#[local] Lemma add_continuous : continuous (fun x : E * E => x.1 + x.2).
+Proof.
+move=> /= [x1 x2] /= A /= [V] /= [V0 filterV0 <-{V}] VA.
+have [W filter0W WV] := split_nbhsbasisat0 filterV0.
+exists ([set x1] `+ W, [set x2] `+ W) => /=.
+split => //=; first by exists ([set x1] `+ W) => //; exists W.
+exists ([set x2] `+ W) => //; exists W => //.
+move => [z1 z2] /= [[x ->]] =>  [[y1] Vy <-{z1}].
+move => [t ->{t}] [y2 Wy2 <-].
+apply: VA => //=.
+exists (x1 + x2) => //; exists (y1 + y2).
+apply: WV =>/=; exists y1 => //; exists y2 =>//.
+by rewrite addrACA.
+Qed.
+
+#[local] Lemma scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2).
+Proof.
+move => /= [r x] /= A /= [_] /= [V fV <-] VA.
+have [r0|] := eqVneq r 0.
+have [V0 fV0 rV0] := (split_nbhsbasisat0 fV).
+have [/= s [s0]] := (absorbing_nbhsbasisat0 fV0 x).
+rewrite inE => xV''.
+have [convV'' balV''] := (absconvex_nbhsbasisat0 fV0 ).
+exists ((ball_ normr 0 (minr 1 s)) (*[set t | `|t| < r]*), [set x] `+ V0) => //=.
+  split.
+   exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //.
+     by rewrite r0.
+   by exists ([set x] `+ V0) => //; exists V0.
+move => [z1 z2] /=; rewrite sub0r normrN => -[z1s].
+move=> [_ ->] [y] Vy <- {z2}; apply: VA => /=; rewrite r0; exists 0; rewrite ?scale0r //.
+exists (z1 *: (x + y)); rewrite ?add0r //.
+apply: rV0 => /=; exists (z1 *: x).
+  apply: (balV'' (z1 * s^-1)).
+    rewrite normrM normfV ltW // ltr_pdivrMr ?normr_gt0 ?gt_eqF //.
+    rewrite mul1r [ltRHS]gtr0_norm // (lt_le_trans z1s) //.
+    by rewrite /minr; case: ifPn => // /ltW //.
+  by exists (s *: x) => //; rewrite !scalerA divfK// gt_eqF //.
+exists (z1 *: y) => //; last by rewrite -scalerDr.
+apply: (balV'' z1); last by exists y.
+rewrite (le_trans (ltW z1s)) // /minr; case: real_ltP => //;
+by rewrite gtr0_real.
+have [V0 fV0 rV0] := (split_nbhsbasisat0 fV).
+have [V' fV' rV'] := (split_nbhsbasisat0 fV0).
+have [V'' fV'' rV''] := (expand_nbhsbasisat0 r fV').
+have [/= s [s0 (*xV'' xx'*)]] := (absorbing_nbhsbasisat0 fV'' x).
+rewrite inE => xV''.
+have [convV'' balV''] := (absconvex_nbhsbasisat0 fV'').
+exists ([set r] `+ (ball_ normr 0 (Num.min `|r| (`|r * s|))) , [set x] `+ V'') => //=.
+  split; last  by exists ([set x] `+ V'') => //; exists V''.
+  exists ((Num.min `|r| (`|r * s|))) => //=.
+  rewrite /minr; case: ifPn; first by rewrite normr_gt0 //.
+    by rewrite normr_gt0 => _ ; rewrite mulf_neq0 // gt_eqF.
+  move=> u/= rur; exists r => //; exists (u - r); last by rewrite subrKC.
+  by rewrite sub0r normrN distrC (lt_le_trans rur)//.
+move => [z1 z2] /= => [] [[x0] -> {x0}] [y]; rewrite add0r normrN => yr.
+move => <- [H ->] [t] Vt <-; apply: VA => /=.
+exists (r *: x) => //; exists (r *: t + y *: x + y *: t); last first.
+  by rewrite !addrA -scalerDr -addrA -scalerDr scalerDl.
+apply: rV0; exists (r *:t) => //.
+  apply: rV'; exists 0; first by apply: mem0_nbhsbasisat0.
+  exists (r *: t); first by apply: rV''; exists t.
+  by rewrite add0r.
+exists (y *: x + y *: t); last by rewrite addrA.
+apply: rV'; exists (y *: x).
+apply: rV''.
+   exists ((r^-1 * y) *: x).
+      apply: (balV'' (r^-1 * y * s^-1)).
+      rewrite -mulrA normrM normfV // ler_pdivrMl ?normr_gt0 // mulr1.
+      rewrite normrM -ler_pdivlMr ?normr_gt0 // ?gt_eqF // ?invr_gt0 //.
+      rewrite (le_trans (ltW yr)) //; rewrite /minr.
+      case: ifPn; last by move=> _; rewrite normfV normrM invrK.
+      by move/ltW; rewrite normrM normfV invrK.
+   exists (s *: x); rewrite // !scalerA divfK//  gt_eqF //.
+   by rewrite scalerA mulrA divff// mul1r.
+exists (y *: t) => //;  apply: rV''; exists ((r^-1 * y) *: t); last first.
+  by rewrite scalerA mulrA divff// mul1r.
+apply: (balV'' (r^-1 * y)); last by exists t.
+rewrite normrM normfV// ler_pdivrMl ?normr_gt0// mulr1.
+by apply: (le_trans (ltW yr)); rewrite /minr; case : real_ltP.
+Qed.
+
+#[local] Lemma locally_convex : exists2 B : set_system E,
+    (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B.
+Proof.
+exists nbhsbasis_at0; first by move=> b; rewrite inE; apply: absconvex_nbhsbasisat0.
+split; first by move=> /= A nA; exists A => //; exists A => //; rewrite addset0.
+move => b [a] /= [a'] fa; rewrite addset0 => <- ab /=.
+by exists a' => //=; split => //; exact: mem0_nbhsbasisat0.
+Qed.
+
+HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R E add_continuous scale_continuous locally_convex.
+
+HB.end.
+
+HB.factory Record Nbhssubbasis0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E := {
+  nbhssubbasis0 : set_system E ;
+  nonempty_nbhssubbasisat0 : exists U, nbhssubbasis0 U;
+  mem0_nbhssubbasisat0 : forall B, nbhssubbasis0 B -> B 0 ;
+  expand_nbhssubbasisat0 : forall B r, nbhssubbasis0 B -> (*0 <= r ->*)
+    exists2 U, nbhssubbasis0 U & r `*: U `<=` B ; (* implies circled *)
+  absorbing_nbhssubbasisat0 : forall B , nbhssubbasis0 B -> pabsorbing_set B;
+  absconvex_nbhssubbasisat0 : forall B, nbhssubbasis0 B -> absolutely_convex_set B }.
+
+Definition nbhs_fromsubbasis0 (R : numFieldType) (E : zmodType)
+    (nbhssubbasis0 : set_system E)  :=
+  finI_from nbhssubbasis0 id.
+
+HB.builders Context R E & Nbhssubbasis0_isConvexTvs R E.
+
+From mathcomp Require Import finmap.
+
+Let nbhsbasis_at0 := @nbhs_fromsubbasis0 R E nbhssubbasis0.
+
+#[local] Lemma nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U.
+Proof.
+have [U fU] := nonempty_nbhssubbasisat0; exists U.
+rewrite /nbhsbasis_at0 /nbhs_fromsubbasis0 /finI_from /=.
+exists [fset U]%fset => /=.
+  by move=> _ /fset1P ->; rewrite mem_set //=; exists U; rewrite ?addset0.
+rewrite /bigcap /=; apply/seteqP; split => z /=; first by apply; rewrite inE. (*bigcap_set1 not working*) by move=> Uz i /fset1P ->.
+Qed.
+
+#[local] Lemma nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V ->
+    exists2 W, nbhsbasis_at0 W & W `<=` U `&` V.
+Proof.
+move=> U V [/= I fI IV] [/=J fJ JU].
+exists (U `&` V) => //.
+exists (I `|` J)%fset.
+ move => /= W; rewrite inE => /orP [WI|WJ]; rewrite mem_set //=.
+   by have := (fI _ WI); rewrite asboolE //=.
+(* extremely hard to understand that asboolE is to be used here *)
+ by have := (fJ _ WJ); rewrite asboolE //=.
+rewrite -IV -JU /bigcap /=; apply/seteqP; split => z /=.
+  by move=> H; split => i iI; apply: H; rewrite inE; apply/orP; [left|right]. (*bigcapI does not work*)
+move => [Iz Jz] i; rewrite inE => /orP [|]; first by apply: Iz.
+by apply: Jz.
+Qed.
+
+#[local] Lemma mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0.
+Proof.
+by move => B [/= I fI <-] U /= /fI /=; rewrite asboolE /= => /mem0_nbhssubbasisat0.
+Qed.
+
+#[local] Lemma expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B ->
+  exists2 U, nbhsbasis_at0 U & r `*: U `<=` B.
+Proof.
+move => B r [/= I fI BI]. (* Change to a type I'*)
+have H : forall i, (i \in I) -> exists2 V, nbhssubbasis0 V & r `*: V `<=` i.
+  move => i /(fI i); rewrite asboolE => /(expand_nbhssubbasisat0 r) /=  [V nV rVi].
+  by exists V.
+pose f i := if (i \in I) =P true is ReflectT h then (sval (cid2 (H _ h))) else setT.
+have Hn i : i \in I -> nbhssubbasis0 (f i).
+ by rewrite /f; case: eqP => // h _; case: cid2.
+have Hr i : i \in I -> r `*: (f i) `<=` i.
+ by rewrite /f; case: eqP => // h _; case: cid2.
+pose U := \bigcap_(i in [set` I])(f i).
+exists U. exists (f @` I)%fset => /=.
+  - by move => _ /imfsetP[/= b bi ->]; apply/mem_set/Hn.
+  - by rewrite set_imfset bigcap_image.
+rewrite -BI => x /= [y]; rewrite /U /= => Uy rx i /= j.
+apply: Hr => //=.
+by exists y => //; apply: Uy.
+Qed.
+
+#[local] Lemma absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B.
+Proof.
+move => B [/= I fI BI] /= x.
+have /= H : forall i, (i \in I) -> exists r : {posnum R}, r%:num *: x \in i.
+  move => i /(fI i); rewrite asboolE => /absorbing_nbhssubbasisat0/(_ x) [r r0 rx].
+  by exists (PosNum r0).
+pose f (i : set E)  : {posnum R} := [elaborate if (i \in I) =P true is ReflectT h then (sval (cid (H i h))) else 1%:pos]. (*elaborate???*)
+have /= Hr i : i \in I -> (f i)%:num *: x \in i.
+ by rewrite /f; case: eqP => // h _; case: cid.
+pose r0 : {posnum R} := [elaborate \big[Order.min/1%:pos]_(i <- I) f i].
+exists r0%:num  => //. (* waouh *)
+rewrite -BI asboolE /= => i /= iI.
+have ni : nbhssubbasis0 i by apply/set_mem/fI.
+have [_ bali] := (absconvex_nbhssubbasisat0 ni).
+apply: (bali (r0%:num / (f i)%:num)).
+ rewrite ger0_norm // ler_pdivrMr // mul1r /r0 num_le //.
+ by apply: ge_bigmin_seq.
+exists ((f i)%:num *: x); first apply/set_mem/Hr => //.
+by rewrite scalerA mulfVK //.
+Qed.
+
+#[local] Lemma absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B.
+Proof.
+move => B [/= I fI <-]; split.
+  move=> x y r; rewrite !asboolE /= => xb yb => // i /= iI.
+  have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [+ _].
+  move=> /(_ x y r); rewrite !asboolE; apply; first by apply: xb.
+  by apply: yb => /=.
+move=> r r1 x /= [y] capy <- i /= iI.
+have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [_ +].
+by move=> /(_ r r1 (r *: y)); apply => /=; exists y => //; apply: capy.
+Qed.
+
+
+HB.instance Definition _ := @Nbhsbasisat0_isConvexTvs.Build R E
+  nbhsbasis_at0 nonempty_nbhsbasisat0 nbhsbasis_at0I mem0_nbhsbasisat0
+  expand_nbhsbasisat0 absorbing_nbhsbasisat0 absconvex_nbhsbasisat0.
+
+HB.end.
+
+
 Section ConvexTvs_numDomain.
-Context (R : numDomainType) (E : convexTvsType R) (U : set E).
+Context (R : numDomainType) (E : convexTvsType R).
 
-Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U).
+Lemma nbhs0N  (U : set E) : nbhs 0 U -> nbhs 0 (-%R @` U).
 Proof. exact/nbhs0N_subproof/scale_continuous. Qed.
 
-Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U).
-Proof. exact/nbhsT_subproof/add_continuous. Qed.
+Lemma nbhsD0  (U : set E) (x :E) : nbhs 0 U -> nbhs x (+%R x @` U).
+Proof. exact/nbhsD_subproof/add_continuous. Qed.
 
-Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U).
+Lemma nbhsD  (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U).
 Proof. exact/nbhsB_subproof/add_continuous. Qed.
 
+Lemma openD  (V : set E) (x : E) : open V -> open ((+%R x @` V)).
+Proof.
+rewrite openE /= => openV z /= [y uy <-]; rewrite /interior /=.
+by apply: nbhsD; rewrite nbhsE /=; exists V => //; split => //; rewrite openE.
+Qed.
+
+Lemma openB (U : set E) (x : E) : open ((+%R x @` U)) -> open U.
+Proof.
+suff  : U = ((+%R (-x) @` (+%R x @` U))) by move => + H; move => ->; apply: openD.
+apply/seteqP; split => z /=.
+  move=> Uz; exists (z + x); first by exists z => //; rewrite addrC.
+  by rewrite -addrCA [X in (_ + X = _)]addrC subrr addr0.
+by move=> [y [y' Uy' <-] <-]; rewrite addrCA addrA subrr add0r.
+Qed.
+
+Lemma nbhsE0 (x : E) (b : set E): nbhs x b <-> b x /\ exists2 a, nbhs 0 a & ([set x + x0 | x0 in a]) `<=` b.
+Proof.
+split.
+  move => /[dup] /(nbhsD (-x)); rewrite addNr => nb0 nb; split; first by apply: nbhs_singleton.
+  exists [set - x + x0 | x0 in b] => // z /=.
+  by move=> [y /= [y' by']] <- <-; rewrite addrA addrN add0r.
+move=> [bx [a n0a xab]]; apply: filterS; first by exact: xab.
+by apply: nbhsD0.
+Qed.
+
 End ConvexTvs_numDomain.
 
 Section ConvexTvs_numField.
@@ -667,8 +1187,43 @@ 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.
 
+Lemma openZ (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) :
+  r != 0 -> open U -> open ( *:%R r @` U ).
+Proof.
+move=> r0; rewrite openE /interior /= => openU z /= [x Ux <-]; apply: nbhsZ => //.
+by rewrite nbhsE => /=; exists U => //; split; rewrite // openE.
+Qed.
+
 End ConvexTvs_numField.
 
+
+Section ConvexTvs_realType.
+
+(*better naming ?*)
+Lemma scalerx_continuous (R : realType) (E : convexTvsType R) (x : E) (s : R) :
+  {for s, continuous (fun t : R^o =>  t *: x)}.
+Proof.
+have -> : (fun t : R^o =>  t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)) by apply: funext.
+apply: continuous_comp.
+apply: (@cvg_pair _ R^o _ _ (nbhs (s : R^o))) => //=; first by exact: cvg_cst.
+by exact: (scale_continuous (s : R^o,x)).
+Qed.
+
+(* why is cvg_cst defined only on realtypes ? *)
+
+Lemma scalexr_continuous (R : realType) (E : convexTvsType R) (x : E) (s : R) :
+  {for x, continuous (fun y : E =>  s *: y)}.
+Proof.
+have -> : (fun y: E =>  s *: y ) = (fun z => z.1 *: z.2) \o (fun y => (s, y)).
+  by apply: funext.
+apply: continuous_comp.
+apply: (@cvg_pair _ R^o _ _ (nbhs (s : R^o))) => //=; first by exact: cvg_cst.
+by exact: (scale_continuous (s: R^o, x)).
+Qed.
+
+End ConvexTvs_realType.
+
+
 Section standard_topology.
 Variable R : numFieldType.
 
@@ -693,6 +1248,7 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
+
 Let standard_ball_convex_set (x : R^o) (r : R) : convex_set (ball x r).
 Proof.
 apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
@@ -706,14 +1262,27 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
 by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
+Let standard_ball_balanced_set (r : R) : balanced_set (ball (0 : R^o) r).
+Proof.
+move => t /= t1 z /= [y].
+rewrite -ball_normE /= !sub0r !normrN => + <-.
+rewrite normrM.
+case: (eqVneq `|t| (1 : R)).
+  by move=> -> ; rewrite mul1r.
+move=> t11.
+have : (`|t| <1) by rewrite lt_neqAle; apply/andP; split.
+by move => lt1 yr; rewrite -[ltRHS]mul1r ltr_pM ?normr_ge0.
+Qed.
+
 Let standard_locally_convex_set :
-  exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B.
+  exists2 B : set_system R^o, (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B.
 Proof.
-exists [set B | exists x r, B = ball x r].
-  by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set.
-split; first by move=> B [x] [r] ->; exact: ball_open.
-move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
-by exists (ball x r) => //=; split; [exists x, r|exact: ballxx].
+exists [set B | exists2 r, (0 < r) & B = ball 0 r].
+   move=> B/= /[!inE]/= [] [r _ ->]; split; first by  exact: standard_ball_convex_set.
+   by exact: standard_ball_balanced_set.
+split; first by move=> /= ? [r r0 ->]; apply: nbhsx_ballx.
+move=>  B [] r /= r0 /= Br; exists (ball 0 r) => /=; last by exact: Br.
+by exists r.
 Qed.
 
 HB.instance Definition _ :=
@@ -753,28 +1322,32 @@ by move=> [l [e f]] /= [] [Al Bl] [] Ae Be; apply: nU; split;
 Qed.
 
 Local Lemma prod_locally_convex :
-  exists2 B : set_system (E * F), (forall b, b \in B -> convex_set b) & basis B.
+  exists2 B : set_system (E * F), (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis (0,0) B.
 Proof.
-have [Be Bcb Beb] := @locally_convex K E.
-have [Bf Bcf Bfb] := @locally_convex K F.
-pose B := [set ef : set (E * F) | open ef /\
+have [Be Bce [Be0 Beb]] := @locally_convex K E.
+have [Bf Bcf [Bf0 Bfb]] := @locally_convex K F.
+pose B := [set ef : set (E * F) |
   exists be, exists2 bf, Be be & Bf bf /\ be `*` bf = ef].
-have : basis B.
-  rewrite /basis/=; split; first by move=> b => [] [].
-  move=> /= [x y] ef [[ne nf]] /= [Ne Nf] Nef.
-  case: Beb => Beo /(_ x ne Ne) /= -[a] [] Bea ax ea.
-  case: Bfb => Bfo /(_ y nf Nf) /= -[b] [] Beb yb fb.
-  exists [set z | a z.1 /\ b z.2]; last first.
-    by apply: subset_trans Nef => -[zx zy] /= [] /ea + /fb.
-  split=> //=; split; last by exists a, b.
-  rewrite openE => [[z z'] /= [az bz]]; exists (a, b) => /=; last by [].
-  rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo.
-  by exists b => //; split => // []; exact: Bfo.
-exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-.
-move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2].
+have lem : nbhs_basis (0,0) B.
+  split.
+    by move=> b [be [bf] /Be0 nbe [/Bf0 nbf] <-]; exists (be,bf); first by split.
+  move=> /= b [/= [be bf]] [/= nbe nbf] /= befb /=.
+  have [/= be' Beb' bbe] := Beb be nbe.
+  have [/= bf' Bfb' bbf] := Bfb bf nbf.
+  exists (be' `*` bf') => /=.
+  exists be'; exists bf' => //.
+  move=> z /= [ bez bfz]; apply: befb; split; first by apply: bbe.
+  by apply: bbf.
+exists B => // => b; rewrite inE /= => [[]] be [] bf Bee [] Bff <-.
+have [convbe balbe] := Bce be (mem_set Bee).
+have [convbf balbf] := Bcf bf (mem_set Bff).
 split.
-  by apply/set_mem/Bcb; [exact/mem_set|exact/mem_set|exact/mem_set].
-by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set].
+  move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2];split.
+  by apply/set_mem/convbe;[exact/mem_set|exact/mem_set].
+  by apply/set_mem/convbf;[exact/mem_set|exact/mem_set].
+move=> r [r1 [x1 y1]] [[x2 y2]]/= [bex bfy] [] <- <-; split.
+  by apply/balbe; [exact: r1|exists x2].
+  by apply/balbf; [exact: r1|exists y2].
 Qed.
 
 HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build
@@ -952,3 +1525,723 @@ Lemma lcfun_linear : linear f.
 Proof. move => *; exact: linearP. Qed.
 
 End lcfunproperties.
+
+Import Norm.
+
+Definition gauge_fun  (K : realType) (V : lmodType K) (A : set V)
+  (absA :  absolutely_convex_set A) (absorbA: pabsorbing_set A)
+  : V -> K :=
+fun v => inf [set r | (0 < r) /\  v \in (fun x => r *: x) @` A].
+
+
+(* K can be a numDomainType once #1959 is solved *)
+(*Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) : V -> \bar K
+    := fun v => ereal_inf (EFin @` [set r | 0 < r /\ v \in (fun x => r *: x) @`A]). *)
+
+Section gauge.
+Context (K : realType) (V : lmodType K) (A : set V) (absA :  absolutely_convex_set A) (absorbA: pabsorbing_set A).
+
+Notation gauge_fun := (gauge_fun absA absorbA).
+
+#[local] Lemma gauge0: gauge_fun 0 = 0.
+Proof.
+have/absolutely_convex0 := absA =>  A0; rewrite /gauge_fun.
+have [->|]:= eqVneq A set0.
+  rewrite [X in inf X]( _ : _ = set0).
+  by rewrite  -subset0 => /= x /=; rewrite image_set0 inE => -[] //.
+  by rewrite inf0.
+set P := (X in inf X).
+move/set0P/A0 => {}A0.
+apply/eqP; rewrite eq_le; apply/andP; split; last first.
+  apply: lb_le_inf.
+    by  exists 1; rewrite /P /=; split => //; rewrite inE; exists 0; rewrite ?scaler0 //; apply: A0.
+  by move=> z; rewrite /P /= => -[z0] _; rewrite ltW.
+have infle : forall (r : K), (0 < r) ->  inf P <= r.
+  move => r r0.
+  have Pr : P r by split => //; rewrite inE; exists 0 => //; rewrite scaler0.
+  apply: ge_inf => //; exists 0 => z /= [] z0 _; rewrite ltW //.
+by apply/ler_addgt0Pl => /= r r0; rewrite addr0; apply: infle.
+Qed.
+
+Lemma gauge_ge0 : forall x, 0 <= gauge_fun x.
+Proof.
+move => v. rewrite /gauge_fun.
+set P := (X in inf X).
+case : (EM (P !=set0)).
+  by move=> H; apply: lb_le_inf => // z; rewrite /P /= => -[] z0 _; rewrite ltW.
+move/nonemptyPn -> ;  rewrite  /inf /=.
+have -> : [set - (x : K) | x in set0] = set0 by rewrite seteqP; split => // x [] //=.
+by rewrite sup0 oppr0.
+Qed.
+
+(*TO BE MOVED to reals *)
+Lemma supS (B : set K) (C : set K) : B !=set0 -> has_sup C -> B `<=` C -> sup B <= sup C.
+Proof.
+move=> B0 supC BC.
+apply: sup_le => //.
+apply: subset_trans; first by exact: BC.
+by exact: le_down.
+Qed.
+
+Lemma infS (B : set K) (C : set K) : has_inf B -> C !=set0 -> C `<=` B -> inf B <= inf C.
+Proof.
+move=> infB C0 BC.
+rewrite /inf lerN2.
+apply: supS; first by apply/nonemptyN.
+by apply/has_inf_supN.
+by apply: image_subset.
+Qed.
+(* END TO BE MOVED *)
+
+
+(* TODO : factorise*)
+#[local] Lemma ler_gaugeD:
+  forall x y, gauge_fun (x + y) <=  gauge_fun x +  gauge_fun y.
+Proof.
+have A0 : A 0 by move: (absorbA 0)=> [??]; rewrite scaler0 inE.
+have :=  absA; rewrite /absolutely_convex_set => -[] convA /= balA.
+have lem (w : V) : (exists2 r, (0 < r) & A (r *: w)) -> has_inf [set t | 0 < t /\ w \in t `*: A].
+  move => [r r0 Aw]; split => /=; rewrite /set0P; last by exists 0 => z [z0 _]; rewrite ltW.
+  exists r^-1 => //=; split=> //.
+  rewrite ?invr_gt0 //.
+  rewrite inE /=; exists (r *: w) => //.
+  by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //.
+move => x y; rewrite /gauge_fun.
+have:= (absorbA x) => -[/= r r0]; rewrite inE /= => Arx.
+have:= (absorbA y) => -[/= r' r0']; rewrite inE /= => Ary.
+have:= (absorbA (x+y)) => -[/= r2 r20']; rewrite inE /= => Arxy.
+rewrite -inf_sumE; first by apply: lem; exists r.
+  by apply: lem; exists r'.
+apply: infS; first by apply: lem;  exists r2.
+  exists (r^-1 + r'^-1) => /=.
+  exists r^-1 => //=.
+    split=> //; rewrite ?invr_gt0 //.
+    rewrite inE /=; exists (r *: x) => //.
+    by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //.
+  exists r'^-1 => //=.
+  split=> //; rewrite ?invr_gt0 //.
+  rewrite inE /=; exists (r' *: y) => //.
+  by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //.
+move => z /= [t [t0]]; rewrite inE /= => [[v] Av rvx] [s] [s0]; rewrite inE /=.
+move => [w Aw twy] <-. rewrite addr_gt0 => //; split => //; rewrite inE /=.
+rewrite -twy -rvx.
+exists  ((t + s)^-1 *: (t *: v + s *: w)).
+rewrite scalerDr !scalerA mulrC (mulrC _ s).
+rewrite -divD_onem => //.
+pose st := Itv01 (mathcomp_extra.divDl_ge0 (ltW t0) (ltW s0))
+                      (mathcomp_extra.divDl_le1 (ltW t0) (ltW s0)).
+have := convA v w st.
+rewrite !inE => /(_ Av Aw); rewrite /conv /=; apply.
+by rewrite !scalerA divff ?scale1r //; rewrite gt_eqF // addr_gt0.
+Qed.
+
+Lemma ge0_infZl : forall (B : set K) [a : K], 0 <= a -> inf [set a * x | x in B] = a * inf B.
+Proof.
+move => B a a0; rewrite /inf mulrN -(ge0_supZl (-%R @` B) a0); congr (- sup _).
+by rewrite !image_comp/=; apply: eq_imagel => //= ? _; rewrite mulrN.
+Qed.
+
+Lemma inf_ge0  (B : set K) : (forall x, B x -> 0 <= x) -> 0 <= inf B.
+Proof.
+move=> B0; have [->|B0'] := eqVneq B set0; first by rewrite inf0.
+by apply: lb_le_inf => //; exact/set0P.
+Qed.
+
+Lemma inf_pos : inf [set r : K | 0 < r] = 0.
+Proof.
+apply/eqP; rewrite eq_le; apply/andP; split; last first.
+  by apply: inf_ge0 => x /ltW.
+apply/ler_addgt0Pr => e e0; rewrite add0r.
+apply: ge_inf => //=.
+by exists 0 => r /ltW.
+Qed.
+
+(* see coq-robot/ode_common.v *)
+#[local] Lemma gaugeZ r v : gauge_fun (r *: v) = `|r| * gauge_fun v.
+Proof.
+rewrite /gauge_fun; have [->|] := eqVneq r 0.
+  rewrite normr0 mul0r.
+  have A0 : A 0 by move: (absorbA 0)=> [??]; rewrite scaler0 inE.
+  rewrite [X in inf X](_ : _ = [set r0 | 0 < r0]).
+    apply/seteqP; split=> [s []//|s /= s0]/=; split => //.
+    by rewrite inE/=; exists 0 => //; rewrite scale0r scaler0.
+  exact: inf_pos.
+rewrite neq_lt -ge0_infZl// => /orP[r0|r0]; congr inf.
+- rewrite ltr0_norm//.
+  have balA w : A w -> A (- w).
+     move=> Aw; case: absA => _ /(_ (-1)); apply => /=; first by rewrite normrN1.
+     by exists w => //; rewrite scaleN1r.
+  apply/seteqP; split => [x [x0 /[!inE]-[w Aw xwry]]|_ [y [y0 /[!inE]-[w Aw <-{v} <-]]]]/=.
+    exists ((- r)^-1 * x); last by rewrite invrN mulrA mulrNN divff ?mul1r// lt_eqF.
+    rewrite mulr_gt0// ?invr_gt0 ?oppr_gt0//; split => //.
+    rewrite inE/=; exists (- w); first exact: balA.
+    rewrite scalerN invrN mulNr scaleNr opprK -scalerA xwry scalerA.
+    by rewrite mulVf ?scale1r ?lt_eqF.
+  rewrite inE/= mulr_gt0 ?oppr_gt0//; split => //.
+  exists (- w); first exact: balA.
+  by rewrite scalerN mulNr scaleNr opprK scalerA.
+- rewrite gtr0_norm//.
+  apply/seteqP; split => [x [x0 /[!inE]-[w Aw xwry]]|_ [y [y0 /[!inE]-[w Aw <-{v} <-]]]]/=.
+    exists (r^-1 * x); last by rewrite mulrA divff ?mul1r// gt_eqF.
+    rewrite mulr_gt0 ?invr_gt0 ?gt_eqF//; split => //.
+    rewrite inE/=; exists w => //.
+    by rewrite -[LHS]scalerA xwry scalerA mulVf ?scale1r// gt_eqF.
+  rewrite inE/= mulr_gt0//; split => //.
+  by exists w => //; rewrite scalerA.
+Qed.
+
+HB.instance Definition _ := @isSemiNorm.Build  K V gauge_fun gauge0 gauge_ge0 ler_gaugeD gaugeZ.
+
+Check (gauge_fun : SemiNorm.type V).
+End gauge.
+
+
+Definition seminorm_on {R : realFieldType} {E : lmodType R} {P : set (SemiNorm.type E)} (Hp : P !=set0) : Type := E.
+
+
+(* TBD squeeze_cvgr once available *)
+Section foo.
+Context {T : Type} {a : set_system T} {Fa : Filter a} {R : realFieldType}.
+Implicit Types f g h : T -> R.
+
+Lemma squeeze_cvgr f h g : (\near a, f a <= g a <= h a) ->
+  forall (l : R), f @ a --> l -> h @ a --> l -> g @ a --> l.
+Admitted.
+End foo.
+
+Section convex_topology_seminorm.
+Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) (H : P !=set0).
+
+HB.instance Definition _ := GRing.Lmodule.on (@seminorm_on R E P H).
+
+Definition seminorm_subbasis :=
+[set A | exists2 p, (P p) & exists2 e, (0 < e) & (A = p @^-1` (ball (0 : R) e))] : set_system E.
+
+Lemma nonempty_subbasis : exists B, seminorm_subbasis B.
+Proof.
+move : H => [p] Pp.
+exists (p @^-1` (ball (0 : R) 1)).
+by exists p => //; exists 1.
+Qed.
+
+Lemma mem0_seminorm_subbasis : forall B, seminorm_subbasis B -> B 0.
+Proof.
+by move=> B; rewrite /seminorm_subbasis /= => -[p Pp [e]] e0 -> /=; rewrite norm0; exact: ballxx.
+Qed.
+
+Lemma split_seminorm_subbasis :
+  forall B, seminorm_subbasis B -> exists2 C, seminorm_subbasis C & ( C `+ C  `<=` B).
+Proof.
+move=> B; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=.
+exists (p @^-1` (ball (0 : R) (e/2))); first by exists p => //; exists (e/2); rewrite ?divr_gt0.
+rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]; rewrite sub0r normrN => ballx [y].
+rewrite sub0r normrE => bally <-; rewrite (splitr e).
+apply: le_lt_trans; last first.
+  apply: ltrD; first by exact: ballx.
+  by exact: bally.
+(* Beware that now that we opened the Norm module ler_normD refers to semiNorm and not to norm*)
+apply: le_trans; last by apply: Num.Theory.ler_normD.
+have :  p (x + y) <= p x + p y by apply: ler_normD.
+by rewrite ger0_le_norm ?nnegrE ?addr_ge0 ?norm_ge0.
+Qed.
+
+Lemma expand_seminorm_subbasis :
+  forall B r, seminorm_subbasis B -> exists2 U, seminorm_subbasis U & (r `*: U `<=` B).
+move=> B r ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=.
+case: (eqVneq r (0 : R)).
+  move => ->; exists (p @^-1` (ball (0 : R) (e))); first by exists p => //; exists e.
+  by move => z /= [x] _; rewrite scale0r => <-; rewrite norm0; exact: ballxx.
+move=> rneq0.
+exists (p @^-1` (ball (0 : R) (e/`|r|))).
+  by exists p => //; exists (e/`|r|); rewrite ?divr_gt0 // normr_gt0.
+rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]; rewrite sub0r normrN => ballx <-.
+by rewrite normZ normrM normr_id mulrC -ltr_pdivlMr ?normr_gt0.
+Qed.
+
+(* TBA convex *)
+Lemma lt_conv (x y r e : R): 0 <= r -> r <= 1 -> x < e -> y < e -> r * x + r.~ * y < e.
+Proof.
+move => r0 r1 xe ye.
+have [->|] := eqVneq r 0; first by rewrite mul0r /onem subr0 add0r mul1r.
+have [->|] := eqVneq r 1; first by  rewrite mul1r /onem subrr mul0r addr0.
+move=> rneq0 rneq1.
+have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r.
+apply: ltrD.
+rewrite lter_pM2l lt_neqAle; apply/andP; split => //; first by rewrite eq_sym.
+by move: xe; rewrite lt_def; move/andP => []; rewrite eq_sym //.
+by apply: ltW.
+rewrite lter_pM2l /onem ?subr_gt0 ?ltW //.
+by rewrite lt_def; apply/andP; split => //; rewrite eq_sym.
+Qed.
+
+Lemma le_conv (x y r e : R):
+0 <= r -> r <= 1 -> 0 <= x -> x <= e -> 0 <= y -> y <= e -> r * x + r.~ * y <= e.
+Proof.
+move => r0 r1 x0 xe y0 ye.
+rewrite /onem.
+have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r.
+apply: lerD; first by rewrite ler_pM.
+by rewrite ler_pM ?subr_ge0 //.
+Qed.
+
+
+Lemma convex_seminorm_subbasis: forall B, seminorm_subbasis B -> convex_set B.
+Proof.
+move=> B ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] x y r.
+rewrite !inE /ball /= !sub0r !normrN => px py.
+rewrite /conv /=.
+have lem1:
+`|p (r%:num *: x + (r%:num).~ *: y)| <= `|p (r%:num *: x) +  p ((r%:num).~ *: y)|.
+ rewrite (@ger0_le_norm _   (p (r%:num *: x + (r%:num).~ *: y)))  ?nnegrE  ?norm_ge0 ?ler_normD //.
+   by rewrite ?nnegrE ?addr_ge0 ?norm_ge0 ?ler_normD//.
+apply:le_lt_trans; first by exact: lem1.
+apply: le_lt_trans; first by apply: Num.Theory.ler_normD.
+rewrite !normZ !normrM !normr_id [X in X*_]ger0_norm //.
+rewrite [X in _ + X*_]ger0_norm ?onem_ge0 //.
+by apply: lt_conv.
+Qed.
+
+
+Lemma balanced_seminorm_subbasis: forall B, seminorm_subbasis B -> balanced_set B.
+Proof.
+move => _ [p Pp [r r0] ->] /= s s1 z /= [x].
+rewrite /ball /ball_ /= !sub0r !normrN => pixr <-.
+rewrite normZ normrM normr_id.
+apply: le_lt_trans; last by exact: pixr.
+by rewrite ler_piMl ?normr_ge0.
+Qed.
+
+Lemma absolutely_convex_seminorm_subbasis: forall B, seminorm_subbasis B -> absolutely_convex_set B.
+Proof.
+move => b Bb; split; first by apply: convex_seminorm_subbasis.
+by apply: balanced_seminorm_subbasis.
+Qed.
+
+Lemma absorbing_seminorm : forall B , seminorm_subbasis B -> pabsorbing_set B.
+move => _ [p Pp [r r0] ->] /= y.
+case: (eqVneq (p y) 0) => y0.
+  by exists 1 => //; rewrite scale1r inE /ball/ball_ /= sub0r normrN y0 normr0.
+exists (r/2 * (p y)^-1).
+  by rewrite !divr_gt0 // lt_neqAle eq_sym norm_ge0; apply/andP.
+(*normr_gt0 not available for seminorms *)
+rewrite inE /ball/ball_ /= sub0r normrN !normZ !normrM !normr_id. Check normrE.
+rewrite !normfV -mulrA mulVf ?normr_eq0 ? mulr1//.
+by rewrite ltr_pdivrMr !gtr0_norm ?ltr_pMr // ltrDr.
+Qed.
+
+HB.instance Definition _ :=  @Nbhssubbasis0_isConvexTvs.Build R (seminorm_on H) seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis expand_seminorm_subbasis absorbing_seminorm absolutely_convex_seminorm_subbasis.
+
+Check (seminorm_on H : convexTvsType R).
+
+(* NB: Using init-fam (see initial_topology.v) doesn't work as we strongly need a 0 basis. With init-fam we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| <e]], while working from a 0 basis gives us nbhs a = [A : set E |, exists e , A = [x | p(x -a) < e]]. In particular, the continuity of the addition can't be proved in the first case*)
+
+From mathcomp Require Import finmap.
+
+Import Norm.
+
+Lemma continuousat0_seminorm : forall p, P p -> continuous_at 0 (p : seminorm_on H -> R).
+Proof.
+move=> p Pp /= /= A [r /= r0] pxrA.
+exists (p @^-1` (ball (p(0) : R) r)) => /=; last first.
+  by move=> z /=; apply: pxrA.
+exists  (p @^-1` (ball (0 : R) r)) => /=.
+  exists ([fset (p @^-1` ball (0 : R) r)]%fset) => /=.
+    move => t; rewrite inE => /eqP ->. rewrite mem_set //.
+    by exists p => //;  exists r.
+  apply/seteqP; rewrite /bigcap; split =>  y //=.
+    by move => /(_ (p @^-1` ball (0 : R) r)); rewrite inE; apply.
+  by move => bxr i; rewrite inE => /eqP -> /=.
+apply/seteqP; split => z /=.
+  move => [? ->] [y]; rewrite /ball /= => bry <- /=; rewrite /ball /=.
+  by rewrite norm0 (add0r y).
+by rewrite norm0 => b0rp; exists 0 => //; exists z => //; rewrite add0r.
+Qed.
+
+Lemma continuous_seminorm x : forall p, P p -> continuous_at x (p : seminorm_on H -> R).
+Proof.
+move=> p Pp.
+suff: (p y - p x)@[y --> x] --> (0 : R).
+  move=> pypx A [r r0] /= pxrA.
+  have npA := (pypx (ball (0 : R^o) r) (nbhsx_ballx (0 : R) r r0)) => /=.
+  exists ([set x] `+ (p @^-1` (ball (0: R) r))) => /=.
+    exists (p @^-1` (ball (0: R) r)) => //.
+    exists ([fset p @^-1` (ball (0 : R) r)]%fset) => //.
+      move => y; rewrite inE => /eqP ->; rewrite mem_set //.
+      by exists p => //; exists r => //=.
+    apply/seteqP; split => t /=.
+      rewrite /bigcap /= => /(_  (p @^-1` (ball (0 : R) r))).
+      by apply; rewrite inE.
+    by move =>   h; rewrite /bigcap /= => ?; rewrite inE => /eqP -> /=.
+  move => t /= [? ->] [y] bally <-; apply: pxrA => /=. rewrite (le_lt_trans _ bally) => //.
+  rewrite sub0r normrN [leRHS]ger0_norm ?norm_ge0 //.
+  by rewrite (le_trans (Theory.seminorm_normrB p _ _)) //  opprD addrA subrr add0r Theory.normN //.
+have nearp : (\forall y \near (nbhs x), -p(y - x) <= p(y) - p(x) <= p (y -x)).
+ apply: nearW => //= y.
+ by have := (Theory.seminorm_normrB p y x); rewrite ler_norml.
+have lem :  (p \o +%R^~ (- x)) x0 @[x0 --> nbhs x] --> (0 : R).
+  apply: (@cvg_comp _ _ _ (fun y => y - x) p); last first.
+    by rewrite -(@norm0 _ _ p); apply: (continuousat0_seminorm Pp).
+  by rewrite -(subrr x)=> A /= /continuous_shift; apply.
+apply: (@squeeze_cvgr _ (nbhs x)) => /=; first by exact: nearp.
+  rewrite -oppr0; apply: (@cvgN _ R^o (seminorm_on H) _ _ (p \o (fun y => y - x))).
+  by exact: lem.
+by apply: lem.
+Qed.
+
+End convex_topology_seminorm.
+
+Section generating_seminorm.
+Context (R : realType) (E : convexTvsType R).
+
+Definition nbhs_of := sval (cid2 (@locally_convex _ E)).
+
+(* TODO : convex is enough and then take balanced closure *)
+Lemma open_nbhs_basis : exists2 B : set (set E),
+  nbhs_basis 0 B & ( forall b, B b -> (open b /\ absolutely_convex_set b)).
+Proof.
+have [absconv [] nbhs0 basis] :=  (svalP (cid2 (@locally_convex _ E))).
+exists [set b| exists2 b', nbhs_of b' & b = interior b'].
+  split => /= a /=; first by move => [b /nbhs0 nbhsb ->]; apply: nbhs_interior.
+  move=> /basis /= [b /= nbhsb ba]; exists (interior b); first by exists b => //.
+  apply: subset_trans; last by exact: ba.
+  exact: interior_subset.
+move=> ? /=  [b nb ->]; split; first by exact: open_interior.
+have [convb balb] := absconv b (mem_set nb).
+split; rewrite /interior.
+  move => x y t; rewrite !inE.
+  move=> /nbhsE0 [bx [ax nax axb]] /nbhsE0 [by' [ay nay ayb]]; apply/nbhsE0; split.
+  by apply/set_mem/convb; rewrite !inE.
+  exists (ax `&` ay); first by apply: filterI.
+  move=> z /= [z' [xz xz'] <-].
+  (*have -> : conv t x y + z' = conv t (x + z') (y + z').*) (*souci avec conv t (x+x0) (y+y0)*)
+  rewrite /conv /=.
+  have ->:  t%:num *: x + (t%:num).~ *: y + z' = t%:num *: (x + z') + (t%:num).~ *: (y + z').
+    rewrite !scalerDr -[in RHS]addrA.
+    rewrite [in X in (_ =  _ + X)]addrCA  [in X in (_ =  _ + ( _ + X))]scalerBl.
+    by rewrite [in X in (_ =  _ +  ( _ + X))]addrCA addrN addr0 scale1r addrA.
+  apply/set_mem/convb; rewrite inE; first by apply: axb; exists z'.
+  by apply: ayb; exists z'.
+move=> /= t.
+case: (eqVneq t 0). (*disctinction overlooked in the literature*)
+  by move=> -> _ ? /= [?]  _; rewrite scale0r => <-; apply: nbhs0 => /=; exact: nb.
+move=> t0 t1 ? /= [x] /= + <-; move/nbhsE0 => [bx [a na0 ab]].
+apply/nbhsE0; split.
+  apply: balb; first by exact: t1.
+  by exists x.
+exists (t `*: a).
+  by rewrite -(@scaler0 _ _ t); apply: nbhsZ => // ? /= [y ay] <-; apply: ab; exists y.
+move => z /= [?] [y] ax <- <-; rewrite -scalerDr; apply: balb; first by exact: t1.
+by exists (x + y)=> //; apply: ab; exists y.
+Qed.
+
+#[local] Definition open_nbhs_of := sval (cid2 open_nbhs_basis).
+
+#[local] Definition open_absconvex_nbhs_of := (svalP (cid2 open_nbhs_basis)).2.
+
+#[local] Definition basis_nbhs_of := (svalP (cid2 open_nbhs_basis)).1.
+
+Lemma basis_neqset0 (B : (set (set  E))) (x : E): (filter_from [set U | B U] id --> x) -> B !=set0.
+Proof.
+by move=> /(_ [set: E]) /(_ filterT) [b ? _]; exists b.
+Qed.
+
+Lemma absorbing_nbhs_of : forall b, open_nbhs_of b -> pabsorbing_set b.
+Proof.
+rewrite /open_nbhs_of => b Bb x.
+have [/(_ b Bb) n0b _] := (basis_nbhs_of ).
+move: n0b; rewrite -(scale0r x) => n0b.
+have := scalerx_continuous => /(_ _ _ x 0 b n0b) [r] /= r0 b0rb.
+exists (r/2); first by apply: divr_gt0.
+rewrite inE.
+apply: b0rb; rewrite /ball_ /= sub0r normrN normrM !gtr0_norm //.
+by rewrite gtr_pMr // invf_lt1 // ltrDl.
+Qed.
+
+Definition seminorm_of  := [set p : SemiNorm.type E | exists b, exists h : (open_nbhs_of b),
+                         p = gauge_fun (open_absconvex_nbhs_of  h).2 (absorbing_nbhs_of h)].
+
+#[local] Lemma seminorm_ofneq0 : seminorm_of !=set0.
+Proof.
+have [_ /(_ [set: E] filterT)] := basis_nbhs_of; move=> [/= b Bb _].
+exists (gauge_fun (open_absconvex_nbhs_of Bb).2 (absorbing_nbhs_of Bb)).
+by exists b; exists Bb.
+Qed.
+
+#[local] Notation seminormE := (@seminorm_on R E seminorm_of seminorm_ofneq0 : convexTvsType R).
+
+Let ball_gauge_fun (A : set E) (r : R) (r0 : 0 < r)
+  (absA : absolutely_convex_set A) (pabsA: pabsorbing_set A) (oA: open A):
+ (gauge_fun absA pabsA) @^-1` (ball (0 : R) r) = (fun y : E =>  r^-1 *: y) @^-1` A.
+Proof.
+apply/seteqP; split => y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0 //.
+  move/inf_lt => [].
+  have := pabsA y => -[r' r'0]; rewrite inE => r'yb.
+  exists r'^-1 => /=; split; first by rewrite invr_gt0.
+    rewrite inE /=; exists (r'*: y) => //.
+    by rewrite scalerA mulrC divff ?scale1r ?lt0r_neq0.
+  move=> t [t0]; rewrite inE => /= -[y' by' <-] tr.
+  have [_ /(_ (t/r))]:= absA; apply.
+    by rewrite gtr0_norm ?divr_gt0 // ler_pdivrMr // mul1r ltW.
+  by exists y' => //; rewrite scalerA mulrC.
+  move=> Ary.
+  have: exists2 t : R , (0 < t < 1) & (r^-1 *: y \in t `*: A).
+  have /scalerx_continuous : nbhs (1 *: (r^-1 *: y)) A.
+    by rewrite scale1r; apply: open_nbhs_nbhs; split => //.
+  move => [s /= s0] b1s.
+  exists ((1 + `|s|/2 )^-1).
+  rewrite ?invr_gt0 ?addr_gt0 ?mulr_gt0 ?normr_gt0 ?lt0r_neq0 ?invr_gt0 //.
+    apply/andP; split => //.
+    by rewrite invf_lt1 ?ltrDl ?addr_gt0 ?mulr_gt0 ?normr_gt0 ?lt0r_neq0 ?invr_gt0.
+  rewrite inE; exists  ((1 + `|s| / 2) *: (r^-1 *: y)).
+    apply: b1s => /=.
+    rewrite opprD addrA subrr add0r normrN gtr0_norm ?mulr_gt0 ?normr_gt0 //.
+    - by rewrite lt0r_neq0.
+    - by rewrite gtr0_norm ?gtr_pMr ?invf_lt1 ?ltrDl //.
+  by rewrite scalerA mulVf ?scale1r //.
+move=> [t /andP [t0 t1] rytb].
+have lepr:  - (t*r) <= sup [set - x | x in [set r1 | 0 < r1 /\ y \in r1 `*: A]].
+  set B := ( X in _ <= sup  X).
+  have Br : B (- (t * r)).
+    exists (t * r); split => //; rewrite ?mulr_gt0 //.
+    rewrite inE; exists (t^-1 *: (r^-1 *: y)) => //.
+      have := rytb; rewrite inE => -[z bź <-]; rewrite scalerA mulVf ?lt0r_neq0 //.
+      by rewrite scale1r.
+    by rewrite !scalerA mulrAC mulrA mulfV -?mulrA ?mulVf ?lt0r_neq0 ?mul1r ?scale1r //.
+  have: has_ubound B by exists 0 => ? [s [s0 _]] <-; rewrite ltW // oppr_lt0.
+  by move/ub_le_sup/(_ _ Br).
+apply: le_lt_trans; first by rewrite lerNl; exact lepr.
+by rewrite gtr_pMl.
+Qed.
+
+From mathcomp Require Import finmap. (* how to do without *)
+(* TODO : uniformise the usage of `+ or (+%R~ @) withine lemmas *)
+Theorem seminorm_convextvs : continuous (id : E -> seminormE) /\ (continuous (id : seminormE -> E)).
+Proof.
+have [B [Bnbhs Bbasis] Bopen_absconvex] := open_nbhs_basis.
+split=> x a.
+  move=> [/=b [?]] [I /= Ig] /= <- <- /filterS; apply.
+  apply/addx_nbhs.
+  apply: filter_bigI => /= i /Ig /set_mem /= => -[? [b' [nb']]] -> [/= r r0 ->].
+  have [/(_ b' nb') nbhsB _] := basis_nbhs_of.
+  set p := (X in nbhs 0 (X @^-1` ball 0 r)).
+  have -> : (p @^-1` ball (0 : R) r) = (fun y : E =>  r^-1 *: y) @^-1` b'.
+    by apply: ball_gauge_fun => //; exact: (open_absconvex_nbhs_of nb').1.
+  by apply: scalexr_continuous; rewrite scaler0.
+move => /nbhsE0 /=  [ax] /= [b n0b ba].
+have [_  /(_ b n0b) /= [b'/=]] := basis_nbhs_of.
+move=> (*/[dup] /open_absconvex_nbhs_of [ob' absconvb']*) Bb' bb'.
+pose p:= gauge_fun  (open_absconvex_nbhs_of Bb').2 (absorbing_nbhs_of Bb').
+have  /open_absconvex_nbhs_of [ob' absconvb'] := Bb'.
+exists ([set x] `+  p @^-1` ball (0 : R) 1) => /=; last first.
+  rewrite ball_gauge_fun => // z /= [? ->] [y]; rewrite invr1 scale1r => b1y xyz.
+  by apply: ba; exists y => //; apply: bb'.
+exists  (p @^-1` ball (0 : R) 1) => //.
+exists ([fset p @^-1` (ball (0 : R) 1)]%fset).
+  move=> c; rewrite !inE; move/eqP => ->; apply/mem_set => /=.
+  exists p; last by exists 1.
+   by exists b'; exists Bb'.
+rewrite /bigcap; apply/seteqP; split => z /=.
+  by move => /(_ (p @^-1` ball (0: R) 1)); apply; rewrite inE.
+by move => b1z ?; rewrite inE => /eqP ->.
+Qed.
+
+#[local] Definition cst0 : E -> R := fun x => 0.
+#[local] Lemma cst00 : cst0 0 = 0. Proof. by []. Qed.
+#[local] Lemma cst0_ge0 : forall x, 0 <= cst0 x.  Proof. by []. Qed.
+#[local] Lemma  ler_cst0D : forall x y, cst0 (x + y) <= cst0 x + cst0 y.
+  Proof. by move=> x y /=; rewrite addr0. Qed.
+#[local] Lemma cst0Z : forall r x, cst0 (r *: x) = `|r| * cst0 x.
+  Proof. by move=> r x; rewrite mulr0. Qed.
+
+HB.instance Definition _ := @isSemiNorm.Build R E cst0 cst00 cst0_ge0 ler_cst0D cst0Z.
+
+(* we could do without the C, look for the c st B c and c `<=` 2 *:` C *)
+#[local] Lemma lcfun_seminorm0 (l : {scalar E}):
+continuous l -> (exists2 C : R, 0 < C & exists2 p : SemiNorm.type E, continuous p & (forall x, `|l x| <= C * p x)).
+Proof.
+have [Bnbhs Bbasis] := basis_nbhs_of.
+move => /[dup] cl /(_ 0 (ball (0 : R) 1)); rewrite linear0.
+move  => /(_ (nbhsx_ballx (0 : R) 1 ltr01 )) /Bbasis /= [b /= Bb bl].
+have {bl} bl : b `<=` [set t | `|l (t)| < 1].
+  by move => t /bl; rewrite /ball /= sub0r normrN.
+have [_ /(_ 0 b (Bnbhs b Bb))] := seminorm_convextvs.
+move=> n0b.
+pose q : SemiNorm.type E  := gauge_fun (open_absconvex_nbhs_of Bb).2 (absorbing_nbhs_of Bb).
+exists 2 => //; exists q.
+  have -> : (q : E -> R) =  (q : seminormE -> R^o)  \o (id : seminormE -> E) by [].
+  move=> x.
+  have contid : {for x, continuous (id : E -> seminormE)}.
+    by have [contid' _] := seminorm_convextvs; apply: (contid' x).
+  have cq : {for x, continuous (q : seminormE -> R^o)}.
+    by apply: (@continuous_seminorm R^o E seminorm_of _ (id x)); exists b; exists Bb => //=.
+  by apply: (continuous_comp contid cq).
+move => x.
+case : (eqVneq x 0); first by move => ->; rewrite linear0 normr0 mulr_ge0 ?norm_ge0.
+move=> x0.
+case : (eqVneq (q x) 0).
+  move=> qx0. (* case forgotten in the litterature *)
+  suff: (l x) = 0 by move => ->; rewrite normr0 mulr_ge0 ?norm_ge0.
+  move: qx0;  rewrite /q /= /gauge_fun /= => qx0.
+  have lxe (e : R) (e0 : 0 < e) : `|l x | < e.
+    have:= (bl (e^-1*:x)) => /=.
+    rewrite linearZ /= normrM normfV ltr_pdivrMl ?normr_gt0 ?lt0r_neq0 //.
+    rewrite mulr1 (gtr0_norm e0); apply.
+    have hasinf :  has_inf [set r | 0 < r /\ x \in r `*: b].
+      split; last by exists 0 => z /= [] z0 _; apply: ltW.
+      have [r r0] := absorbing_nbhs_of Bb x.
+      move/set_mem => bx.
+      exists r^-1 => /=; split; rewrite ?invr_gt0 //; apply/mem_set.
+      by exists (r *: x) => //; rewrite scalerA ?mulVf ?lt0r_neq0 ?scale1r.
+    have [eps [eps0 /set_mem /= [y by' epsyx]]] := inf_adherent e0 hasinf.
+    rewrite qx0 add0r -epsyx scalerA => epse; rewrite ?mulVf.
+    have /(_ (e^-1 * eps)):= ((open_absconvex_nbhs_of  Bb).2).2.
+    apply => //=; last by exists y.
+    by rewrite ger0_norm  ?mulr_ge0 ?invr_ge0 ?ler_pdivrMl ?ltW ?mulr1.
+  apply: contrapT => /eqP h.
+  have:= lxe `|l x|.
+  by rewrite normr_gt0 ltxx falseE; apply.
+move=> qx0.
+pose y := ((2 * q x)^-1) *: x.
+have : `|l (y)| < 1.
+  apply/bl.
+  have : (q @^-1` ball (0 : R) 1) (((2 * q x)^-1) *: x).
+    move => /=; rewrite sub0r normrN ger0_norm ?norm_ge0 //.
+    rewrite normZ /= ger0_norm ?mulr_ge0 ?invr_ge0 ?norm_ge0 //.
+      by rewrite mulr_ge0 ?norm_ge0 .
+    rewrite invfM -mulrA mulVf // ltr_pdivrMl ?mulr1 ?ltrDl //=.
+    by suff : 0 < 1 :> R by [].
+  rewrite ball_gauge_fun => //; first by have [] := open_absconvex_nbhs_of Bb.
+  by rewrite /= invr1 scale1r.
+rewrite /y linearZ normrM normfV normrM  ger0_norm // ltr_pdivrMl.
+  by rewrite mulr_gt0 ?normr_gt0.
+by rewrite mulr1 [X in _ < _ * X]ger0_norm ?norm_ge0 // => ?; apply: ltW.
+Qed.
+
+(* more complicated proof, done as in the litterature, while the intermediate lemma baule_gauge_fun is useful here *)
+(*
+#[local] Lemma lcfun_seminorm1 (l : {scalar E}):
+continuous l -> (exists2 p : SemiNorm.type E, continuous p & (forall x, `|l x| <= p x)).
+Proof.
+have [B [Bnbhs Bbasis] Bopen_absconvex] := open_nbhs_basis. (* redundant with local notations above but cleaner *)
+move => /(_ 0 (ball (0 : R) 1)); rewrite linear0. 
+move  => /(_ (nbhsx_ballx (0 : R) 1 ltr01 )) /Bbasis /= [b /= Bb bl].
+have {bl} bl : b `<=` [set t | `|l (t)| < 1].
+  by move => t /bl; rewrite /ball /= sub0r normrN.
+have [_ /(_ 0 b (Bnbhs b Bb))] := seminorm_convextvs.
+move=> [x [y [/= I /= Iset] <- <-]]; rewrite addset0 /(_ @^-1` _) /= => Ib {x y}.
+rewrite /seminorm_subbasis /= in Iset.
+have Iseminorm i : i \in I  -> exists2 p : SemiNorm.type E,
+                        seminorm_of p & exists2 e : R, 0 < e & i = (p @^-1` (ball (0 :R) e)).
+  by move/Iset/set_mem.
+pose p i := if (i \in I) =P true is ReflectT h then sval (cid2 (Iseminorm _ h)) else cst0.
+have seminorm_ofp i : i \in I -> seminorm_of (p i).
+ by rewrite /p; case: eqP => // h _; case: cid2.
+have setp i : i \in I -> exists2 e : R, 0 < e & i = (p i)@^-1` ball (0 : R) e.
+ by rewrite /p; case: eqP => // h _; case: cid2.
+pose e i := if (i \in I) =P true is ReflectT h then sval (cid2 (setp _ h)) else 1.
+have eilt0 i : i \in I -> 0 < (e i).
+ by rewrite /e; case: eqP => // h _; case: cid2.
+have eile0 i : 0 <= (e i).
+  by rewrite /e; case: eqP => // h; case: cid2 => //= x x0 _; rewrite ltW.
+have iballe i : i \in I -> i = (p i)@^-1` ball (0 : R) (e i).
+ by rewrite /e; case: eqP => // h _; case: cid2.
+pose emax := \big[Order.max/(0:R)]_(i <- I) e i.
+have emax0 : (0 <= emax) by apply: bigmax_ge_id.
+pose P := fun x =>  2 * (\big[Order.min/(emax)]_(i <- I) e i)^-1 * (\big[Order.max/(0:R)]_(i <- I) (p i x)).
+have P0 : P 0 = 0.
+  have maxp0 : (\big[Order.max/(0:R)]_(i <- I) (p i 0)) = 0.
+    by apply: bigmax_eq_id => i _; rewrite norm0.
+  by rewrite /P maxp0 mulr0.
+have Pge0 : forall x, 0 <= P x.
+  move=> x.
+  by rewrite ?mulr_ge0 ?invr_ge0 ?bigmax_ge_id //; apply: le_bigmin => // i; apply: eile0.
+have ler_PD : forall x y, P (x + y) <= P x + P y.
+  move=> x y; rewrite /P -mulrDr ler_pM ?mulr_ge0 ?invr_ge0 ?bigmax_ge_id //.
+    by apply: le_bigmin => // i; apply: eile0.
+  have [ixy Iix -> ] : {i | i \in I &   \big[maxr/0]_(i <- I) p i (x + y)  = p i (x + y)}.
+  (*how to handle the coercion between i \in I and I : I *)
+  Fail apply: eq_bigmax. admit.
+  have /le_trans : p ixy (x + y) <= p ixy x + p ixy y by apply: ler_normD.
+  apply; apply: lerD.
+    Fail apply/bigmax_geP. admit.
+  Fail apply/bigmax_geP. admit.
+have PZ : forall r x, P (r *: x) = `|r| * P x. admit.
+pose Psaxiom := @isSemiNorm.Build R E P P0 Pge0 ler_PD PZ.
+pose Ps : SemiNorm.type E := HB.pack P Psaxiom.
+exists Ps.
+admit.
+move => x.
+pose y := (Ps x)^-1 *: x.
+have : `|l (y)| < 1.
+  apply/bl/Ib => i /= /[dup] Ii /(iballe i) -> /=.
+  rewrite /y /Ps /P /= /ball /= sub0r normrN.
+  rewrite ger0_norm ?norm_ge0 // normZ.
+  rewrite ger0_norm ?invr_ge0 ?mulr_ge0 ?invr_ge0 ?bigmax_ge_id //.
+    by apply: le_bigmin => // i; apply: eile0.
+  set ex := (X in (2 / X * _)^-1* _ < _).
+  set px := (X in (2 / _ * X)^-1* _ < _).
+  have ex0 : 0 <= ex by apply: le_bigmin => //.
+  have px0 : 0 <= px by rewrite bigmax_ge_id.
+  case: (eqVneq (0 :R) px).
+     by rewrite -mulrA =>  <-; rewrite !mulr0 invr0 mul0r eilt0.
+  case: (eqVneq 0 (p i x)); first by move=> <- _; rewrite mulr0 ?eilt0.
+  case : (eqVneq 0 ex); first by move => <-; rewrite invr0 mulr0 mul0r invr0 mul0r eilt0.
+  move=> exneq0 pineq0 bigneq0.
+  have exgt0 : 0 < ex by  rewrite lt_neqAle; apply/andP; split => //.
+  have pxgt0 : 0 < px by  rewrite lt_neqAle; apply/andP; split => //.
+  have pixgt0 : (0 < (p i x)).
+    by rewrite lt_neqAle; apply/andP; split => //; rewrite norm_ge0.
+  have expxgt0 : 0 < (ex^-1 * px) by rewrite mulr_gt0 ?invr_gt0 //.
+  have lebig : (ex^-1 * px)^-1  * (p i x) <= e i.
+    rewrite invfM invrK [X in X * _ <= _]mulrC -mulrA ler_pdivrMl.
+      by rewrite lt_neqAle; first by apply/andP; rewrite ?norm_ge0.
+    rewrite mulrC ler_pM ?(@ltW _  _(0 : R)) //.
+    - by apply: bigmax_sup_seq; first by exact: Ii.
+    - by rewrite ge_bigmin_seq //.
+  apply: lt_le_trans; last by exact: lebig.
+  rewrite -mulrA invfM -mulrA gtr_pMl ?invf_lt1 ?ltrDl ?mulr_gt0 ?invr_gt0//.
+rewrite /y linearZ normrM normfV (ger0_norm (norm_ge0 _)).
+move=> hyp. (*the following should be simpler ? *)
+have lem : P x = 0 -> l x = 0.
+  move/eqP; rewrite mulf_eq0; move/orP; rewrite mulf_eq0 => -[].
+  move/orP => -[] /eqP h. (*case h doesn´t work ?*) admit.
+    have := @eq_bigmin _ R I _ _ _ _. admit.
+  admit.
+case : (eqVneq (P x) 0).
+  by move => /eqP; move => /eqP/lem ->; rewrite normr0 norm_ge0.
+move=> pneq0.
+rewrite -[X in  X <= _]mul1r -(@divff _ `|Ps x|) ger0_norm //. 
+rewrite -[X in _ <= X]mulr1 -mulrA.
+rewrite ler_pM ?mulr_ge0 ?invr_ge0 ?norm_ge0 ?bigmax_ge_id //.
+ by apply: le_bigmin => // i; apply: eile0. 
+by apply: ltW.
+Admitted.
+*)
+
+#[local] Lemma lcfun_seminorm2 (l : {scalar E}):
+ (exists2 C : R, 0 < C & exists2 p : SemiNorm.type E,  continuous p & (forall x, `|l x| <= C * p x))
+   -> continuous (l : E -> R^o).
+Proof.
+move=> [C C0] [p px lpxl]; apply: continuousfor0_continuous => /= a.
+rewrite linear0 => -[/= e e0] balla.
+have /filterS : (p @^-1`  (ball_ [eta normr] (0 : R) (C^-1 * e)) ) `<=` (l @^-1` a).
+  move=> z /=; rewrite sub0r normrN ger0_norm ?norm_ge0 // => pze.
+  apply: balla => /=; rewrite sub0r normrN.
+  apply: le_lt_trans; first by apply: lpxl.
+  by rewrite -ltr_pdivlMl.
+apply => /=; rewrite -(@norm0 _ _ p); apply: px.
+by rewrite norm0 ; apply: nbhsx_ballx; rewrite mulr_gt0 ?invr_gt0.
+Qed.
+
+Proposition lcfun_seminorm (l : {scalar E}):
+continuous l <->
+ (exists2 C : R, 0 < C & exists2 p : SemiNorm.type E,  continuous p & (forall x, `|l x| <= C * p x)).
+Proof.
+split; first by apply: lcfun_seminorm0.
+by apply: lcfun_seminorm2.
+Qed.
+
+End generating_seminorm.
+
+
+ (* TODO : apply it to hahn banach *)
diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v
index 943c1210c..56c4cc549 100644
--- a/theories/topology_theory/initial_topology.v
+++ b/theories/topology_theory/initial_topology.v
@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat algebra all_classical.
+From mathcomp Require Import all_ssreflect_compat all_algebra all_classical finmap.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import interval_inference reals topology_structure.
@@ -101,6 +101,13 @@ rewrite nbhs_filterE; apply: filterS FC.
 by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image.
 Qed.
 
+Lemma initial_nbhs (x : W) b : nbhs (f x) b -> nbhs x (f @^-1` b).
+Proof.
+rewrite nbhsE /= => -[b' [b0 ob]] bb'.
+exists (f @^-1` b'); split => //= ; first by exists b'.
+by move => z /= /bb'.
+Qed.
+
 End Initial_Topology.
 (*#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed `initial_open`")]
 Notation wopen := initial_open (only parsing).*)
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index a6170e44b..03f4e3ef4 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -125,6 +125,9 @@ Definition open_nbhs (p : T) (A : set T) := open A /\ A p.
 Definition basis (B : set_system T) :=
   B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x.
 
+Definition nbhs_basis (x : T) (B : set (set T)) :=
+  (B `<=` nbhs x) /\ filter_from [set U | B U] id --> x.
+
 Definition second_countable := exists2 B, countable B & basis B.
 
 Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p).
@@ -182,8 +185,8 @@ move=> A B; rewrite openE => Aop Bop p [Ap Bp].
 by apply: filterI; [apply: Aop|apply: Bop].
 Qed.
 
-Lemma bigcup_open (I : Type) (D : set I) (f : I -> set T) :
-  (forall i, D i -> open (f i)) -> open (\bigcup_(i in D) f i).
+Lemma bigcup_open (I : Type) (D : set I) (f : I -> set T) : 
+ (forall i, D i -> open (f i)) -> open (\bigcup_(i in D) f i).
 Proof.
 rewrite openE => fop p [i Di].
 by have /fop fiop := Di; move/fiop; apply: filterS => ??; exists i.
@@ -496,6 +499,11 @@ HB.instance Definition _ := Nbhs_isTopological.Build T
 
 HB.end.
 
+
+Definition open_from (T : Type) (I : Type) (D : set I) (b : I -> set T)
+:= [set \bigcup_(i in D') b i | D' in subset^~ D].
+
+
 (** Topology defined by a base of open sets *)
 
 HB.factory Record isBaseTopological T & Choice T := {
@@ -509,7 +517,7 @@ HB.factory Record isBaseTopological T & Choice T := {
 
 HB.builders Context T & isBaseTopological T.
 
-Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D].
+Local Notation open_from := (open_from D b).
 
 Let open_fromT : open_from setT.
 Proof. exists D => //; exact: b_cover. Qed.