from open_basis to nbhs_basis in tvs

CHANGELOG_UNRELEASED.md

@@ -81,6 +81,9 @@
 - in `measurable_structure.v`:
   + structure `PMeasurable`, notation `pmeasurableType`
 
+- in `topology_structure.v`:
+  + definition `nbhs_basis`
+
 - in `subspace_topology.v`:
   + lemma `withinU_continuous_patch`
 - in `matrix_normedtype.v`:
@@ -137,6 +140,12 @@
 - moved from `topology_structure.v` to `filter.v`:
   + lemma `continuous_comp` (and generalized)
 
+- in `tvs.v`:
+  + structure `convexTvsType` where axiom `locally_convex` uses `nbhs_basis`
+    instead of `basis`
+  + adapted lemmas `standard_locally_convex` and `prod_locally_convex`
+    to `nbhs_basis` instead of `basis`
+
 - in `numfun.v`:
   + `fune_abse` renamed to `funeposDneg` and direction of the equality changed
   + `funeposneg` renamed to `funeposBneg` and direction of the equality changed

theories/normedtype_theory/tvs.v

@@ -387,7 +387,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 -> convex_set b) & (nbhs_basis 0)  B
 }.
 
 #[short(type="convexTvsType")]
@@ -435,7 +435,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 -> convex_set b) & nbhs_basis 0 B
   }.
 
 HB.builders Context R E & PreTopologicalLmod_isConvexTvs R E.
@@ -609,13 +609,14 @@ by rewrite ltrD// ltr_pM2l// onem_gt0.
 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 -> 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 | exists r, B = ball 0 r].
+  by move=> B/= /[!inE]/= [] [r] ->; exact: standard_ball_convex_set.
+move=> B [] r /= r0 /= Br.
+exists (ball 0 r); last by exact: Br.
+split; last by apply: ballxx.
+by exists r. 
 Qed.
 
 HB.instance Definition _ :=
@@ -655,28 +656,28 @@ 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 -> convex_set b) & nbhs_basis (0,0) B.
 Proof.
-have [Be Bcb Beb] := @locally_convex K E.
+have [Be Bce Beb] := @locally_convex K E.
 have [Bf Bcf Bfb] := @locally_convex K F.
-pose B := [set ef : set (E * F) | open ef /\
+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].
-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].
+have lem : nbhs_basis (0,0) B.
+  move=> /= b [/= [be bf] [/= nbe nbf]] /= befb /=.
+  have [/= be' [Beb' be'0] bbe] := Beb be nbe.
+  have [/= bf' [Bfb' bf'0] bbf] := Bfb bf nbf.
+  exists (be' `*` bf').
+  split; first by exists be'; exists bf'.
+  split => //=.
+  apply: subset_trans; last by exact: befb.
+  move => t /= [bet bft]; split; first by apply: bbe.
+  by apply: bbf.
+exists B => // => b; rewrite inE /= => [[]] be [] bf Bee [] Bff <-.
+have convbe := Bce be (mem_set Bee).
+have convbf := Bcf bf (mem_set Bff).
+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].
 Qed.
 
 HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build

theories/topology_theory/topology_structure.v

@@ -120,6 +120,9 @@ Definition open_nbhs (p : T) (A : set T) := open A /\ A p.
 Definition basis (B : set (set T)) :=
   B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x.
 
+Definition nbhs_basis x (B : set (set T)) :=
+  filter_from [set U | B U /\ U x] id --> x.
+
 Definition second_countable := exists2 B, countable B & basis B.
 
 Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p).