evt wip

theories/evt.v

@@ -112,6 +112,18 @@ HB.builders Context R E of TopologicalLmod_isEvt R E.
   Unshelve. all: by end_near.
   Qed.
 
+  Lemma nbhs_add: forall (U : set E) (z :E), forall (x : E), nbhs z U -> nbhs (x + z) (+%R x @`U).
+  Proof.
+  move => U z x U0. 
+  move: (@add_continuous ((x+z)%E,-x) U) => /=. rewrite addrAC subrr add0r.
+  move=> /(_ U0) //=.
+  case=> //= [B] [B1 B2] BU. near=> x0.
+  exists (x0-x); last by rewrite //= addrCA subrr addr0.
+  apply: (BU (x0,-x)); split => //=; last by apply: nbhs_singleton. 
+  by near: x0; rewrite nearE.  
+  Unshelve. all: by end_near.
+  Qed.
+
   Lemma entourage_inv_subproof :
     forall A : set (E * E), entourage A -> entourage A^-1%classic.
   Proof.
@@ -139,9 +151,33 @@ HB.builders Context R E of TopologicalLmod_isEvt R E.
   by apply: (Wadd( (xy.1 - z,z - xy.2))); split => //=.
  Qed.
 
+
 Lemma nbhsE_subproof : nbhs = nbhs_ entourage.
 Proof.
-Admitted. (**)
+rewrite /nbhs_  /=; apply: funext => x; rewrite /filter_from /=.
+apply: funext => U; apply: propext => /=; rewrite /entourage /=; split.
+move=> nU; exists [set xy | U(x  + (xy.1 - xy.2))].
+  exists ((fun z => z-x) @` U); split.
+    rewrite -(addrN x) addrC; move: (nbhs_add (-x) nU).
+    have -> : [set ((- x)%R + x0)%E | x0 in U] = [set z - x | z in U].
+      apply: funext => z /=; apply: propext; split;
+      by move=> [x0 U0]; rewrite addrC=> H; exists x0.
+    by [].
+  move => xy; rewrite !inE /= => [[z] Uz ] <-.
+  by rewrite addrCA subrr addr0.
+move => /= z. (*issue*) admit.
+move=> [A [U0 [NU UA]] H].
+near=> z; apply: H => /=; rewrite -inE; apply: UA => /=.
+near: z; rewrite nearE.
+move: (nbhsT x NU)=> /=.
+have -> : [set (x + x0)%E | x0 in U0] = (fun x0 : E => x - x0 \in U0).
+ apply:funext => z /=; rewrite inE; apply: propext; split.
+  move=> [x0 H <-]; rewrite -opprB -addrAC addrN add0r.
+  admit (*issue*). 
+  move=> Uxz; exists (z-x). admit (*issue*). 
+  by rewrite addrCA subrr addr0.
+by [].
+Admitted.
 
 HB.instance Definition _ := Nbhs_isUniform_mixin.Build E
     entourage_filter entourage_refl_subproof
@@ -159,7 +195,6 @@ HB.mixin Record hasDual (R : ringType) (E' : lmodType R) E of GRing.Lmodule R E
  dual_pair_rlinear : forall x, scalar (dual_pair x);
  dual_pair_llinear : forall x, scalar (dual_pair^~ x);
  ipair : injective ( fun x =>  dual_pair^~ x)
-
 }.   
 
 Section bacasable.