Repair structure names in tvs.v

CHANGELOG_UNRELEASED.md

@@ -12,6 +12,25 @@
     * implemented through a module `ConvexQuasiAssoc` containing
       `law` and helper lemmas
   + lemmas `convR_itv`, `convR_line_path`
+- in `num_topology.v`
+  + `topologicalType` instance on `R^o` for `R : numDomainType`
+
+- in `tvs.v`
+  + HB classes `TopologicalNmodule`, `TopologicalZmodule`, `TopologicalLmodule`
+    `UniformNmodule`, `UniformZmodule`, `UniformLmodule`
+  + notation `topologicalZmodType`
+  + mixin `PreTopologicalNmodule_isTopologicalNmodule`,
+    `TopologicalNmodule_isTopologicalZmodule`,
+    `TopologicalZmodule_isTopologicalLmodule`,
+    `PreUniformNmodule_isUniformNmodule`,
+    `UniformNmodule_isUniformZmodule`,
+    `PreUniformLmodule_isUniformLmodule`
+  + structure `topologicalLmodule`
+  + factories `PreTopologicalNmodule_isTopologicalZmodule`,
+    `TopologicalNmodule_isTopologicalLmodule`,
+    `PreUniformNmodule_isUniformZmodule`,
+    `UniformNmodule_isUniformLmodule`
+  + lemmas `sub_continuous`, `sub_unif_continuous`
 
 ### Changed
 
@@ -59,6 +78,9 @@
 - in `convex.v`:
   + definition `convex_realDomainType` generalized and
     renamed accordingly `convex_numDomainType`
++ in `tvs.v`
+  + HB class `UniformZmodule` now contains `TopologicalZmodule`
+  + HB class `UniformLmodule` now contains `TopologicalLmodule`
 
 ### Renamed
 
@@ -67,6 +89,15 @@
 
 - in `convex.v`
   + lemma `conv_gt0` to `convR_gt0`
+- in `tvs.v`
+  + HB class `TopologicalNmodule` moved to `PreTopologicalNmodule`
+  + HB class `TopologicalZmodule` moved to `PreTopologicalZmodule`
+  + HB class `TopologicalLmodule` moved to `PreTopologicalLmodule`
+  + structure `topologicalLmodule` moved to `preTopologicalLmodule`
+  + HB class `UniformNmodule` moved to `PreUniformNmodule`
+  + HB class `UniformZmodule` moved to `PreUniformZmodule`
+  + HB class `UniformLmodule` moved to `PreUniformLmodule`
+
 
 ### Generalized
 

theories/normedtype_theory/normed_module.v

@@ -131,8 +131,10 @@ by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
 Qed.
 
 HB.instance Definition _ :=
- Uniform_isTvs.Build K V add_continuous scale_continuous locally_convex.
-
+  PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous.
+HB.instance Definition _ :=
+  TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous.
+HB.instance Definition _ := Uniform_isTvs.Build K V locally_convex.
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ.
 

theories/topology_theory/num_topology.v

@@ -26,9 +26,62 @@ Local Open Scope ring_scope.
 HB.instance Definition _ (R : numDomainType) := hasNbhs.Build R^o
   (nbhs_ball_ (ball_ (fun x => `|x|))).
 
+Module TopologicalNumDomainType.
+Section TopologicalNumDomainType.
+Variable (R : numDomainType).
+
+Lemma nbhs_filter (p : R^o) : ProperFilter (nbhs p).
+Proof.
+split.
+  move=> [] e e0 /subsetP/(_ p).
+  by rewrite !in_setE/= subrr normr0.
+split=> [|P Q|P Q].
+- by exists 1; [exact: ltr01|exact: subsetT].
+- move=> [] /= e e0 /subsetP eP [] /= f f0 /subsetP fQ.
+  exists (Order.min e f) => /=.
+    by rewrite [Num.min e f]/(Order.min e f); case: ifP.
+  apply/subsetP => x.
+  rewrite in_setE in_setI/= => pef.
+  apply/andP; split.
+    apply/eP/mem_set/(lt_le_trans pef).
+    by case: (@real_ltP _ e f) => //; exact: gtr0_real.
+  apply/fQ/mem_set/(lt_le_trans pef).
+  by case: (@real_ltP _ f e) => //; exact: gtr0_real.
+- move=> PQ [] /= e e0 eP.
+  by exists e => //; exact: (subset_trans eP).
+Qed.
+
+Lemma nbhs_singleton (p : R^o) (A : set R) : nbhs p A -> A p.
+Proof.
+move=> [] /= e e0 /subsetP /(_ p).
+by rewrite !in_setE/= subrr normr0 e0 => /(_ erefl).
+Qed.
+
+Lemma nbhs_nbhs (p : R^o) (A : set R) : nbhs p A -> nbhs p (nbhs^~ A).
+Proof.
+move=> [] /= e e0 /subsetP eA; exists e => //.
+apply/subsetP => x /[!inE]/= xe.
+exists (e - `|p - x|); first by rewrite /= subr_gt0.
+apply/subsetP => y; rewrite inE/= ltrBrDl => ye.
+apply/eA/mem_set => /=.
+by rewrite -(subrK x p) -addrA (le_lt_trans (ler_normD _ _)).
+Qed.
+
+End TopologicalNumDomainType.
+
+End TopologicalNumDomainType.
+
+HB.instance Definition _ (R : numDomainType) := Nbhs_isNbhsTopological.Build R^o
+  (@TopologicalNumDomainType.nbhs_filter R)
+  (@TopologicalNumDomainType.nbhs_singleton R)
+  (@TopologicalNumDomainType.nbhs_nbhs R).
+
+HB.instance Definition _ (R : numFieldType) := Nbhs_isPseudoMetric.Build R R^o
+  nbhs_ball_normE ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.
+
 HB.instance Definition _ (R : numFieldType) :=
-  Nbhs_isPseudoMetric.Build R R^o
-    nbhs_ball_normE ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.
+  Uniform_isPseudoMetric.Build R R^o
+    ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.
 
 Lemma real_order_nbhsE (R : realFieldType) (x : R^o) : nbhs x =
   filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]).