changelog topology.v

math-comp · Jan 24, 2024 · 7b0fec3 · 7b0fec3
1 parent 3f539de
commit 7b0fec3
Show file tree

Hide file tree

Showing 2 changed files with 201 additions and 3 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -57,6 +57,26 @@
 - in `reals.v`:
   + definition `Rint_pred`
 
+- in `topology.v`
+  + definition `set_system`, identity coercion `set_system_to_set`
+    with instances using `Equality.on`, `Choice.on`, `Pointed.on`,
+	`isFiltered.Build`
+  + mixin `selfFiltered`, factory `hasNbhs`, structure `Nbhs`,
+    type `nbhsType`
+  + instance for matrices using `selfFiltered.Build`
+  + lemmas `cvg_in_ex`, `cvg_inP`, `cvg_in_toP`, `dvg_inP`, `cvg_inNpoint`,
+    `eq_is_cvg_in`
+  + notations `E @[ x \oo ]`, `limn`, `cvgn`
+  + definition `continuous_at`
+  + definitions `weak_topology`, `sup_topology`, `prod_topology`
+  + definition `prod_topo_apply`
+  + definition `discrete_topology`
+  + instead of `zmodType` using `isPointed.Build`
+  + definition `pointwise_cvgE`,
+    instance using `Uniform.copy` for `{ptws _ -> _}`
+  + definition `compact_open_of_nbhs`, lemmas `compact_openK_nbhsE_subproof`,
+    `compact_openK_openE_subproof`
+
 ### Changed
 
 - in `boolp.v`:
@@ -374,6 +394,164 @@
     * lemmas `cvg_series_cvg_series_group`, `lt_sum_lim_series`, `is_cvg_series_sin_coeff`,
 	  `sinE`, `cvg_sin_coeff'`, `is_cvg_series_cos_coeff`, `cosE`, `cvg_cos_coeff'`
 
+- in `topology.v`:
+  + canonicals `linear_eqType`, `linear_choiceType` ->
+    instances using `gen_eqMixin`, `gen_choiceMixin`
+  + canonical `gen_choiceMixin` -> instance using `isPointed.Build`
+  + module `Filtered` (packed class) -> mixin `isFiltered` with field `nbhs`,
+    structure `Filtered`
+  + now use `set_system`:
+    * definitions `filter_from`, `filter_prod`, `cvg_to`, `type_of_filter`, `lim_in`,
+	  `Build_ProperFilter`, `filter_ex`, `fmap`, `fmapi`, `globally`, `in_filter_prod`,
+	  `within`, `subset_filter`, `powerset_filter_from`, `principal_filter`, `locally_of`,
+	  `sup_subbase`, `cluster`, `compact`, `near_covering`, `near_covering_within`,
+	  `compact_near`, `nbhs_`, `weak_ent`, `sup_ent`, `cauchy`, `cvg_cauchy`, `cauchy_ex.Build`,
+	  `cauchy_ball`
+	* classes `Filter`, `ProperFilter'`, `UltraFilter`
+	* instances `fmap_proper_filter`, `fmapi_filter`, `fmapi_proper_filter`,
+	  `filter_prod_filter`, `filter_prod1`, `filter_prod2`
+	* record `in_filter`
+	* structure `filter_on`
+	* variant `nbhs_subspace_spec`
+	* lemmas `nearE`, `eq_near`, `nbhs_filterE`, `cvg_refl`, `cvg_trans`, `near2_curry`,
+	  `near_swap`, `filterP_strong`, `filter_nbhsT`, `nearT`, `filter_not_empty_ex`,
+	  `filter_ex_subproof`, `filter_getP`, `near`, `nearW`, `filterE`, `filter_app`,
+	  `filter_app2`, `filter_app3`, `filterS2`, `filterS3`, `nearP_dep`, `filter2P`,
+	  `filter_ex2`, `filter_fromP`, `filter_fromTP`, `filter_bigIP`, `filter_forall`,
+	  `filter_imply`, `fmapEP`, `fmapiE`, `cvg_id`, `appfilterP`, `cvg_app`, `cvgi_app`,
+	  `cvg_comp`, `cvgi_comp`, `near_eq_cvg`, `eq_cvg`, `neari_eq_loc`, `cvg_near_const`,
+	  `near_pair`, `near_map`, `near_map2`, `near_mapi`, `filter_pair_set`,
+	  `filter_pair_near_of`, `cvg_pair`, `cvg_comp2`, `near_powerset_map`,
+	  `near_powerset_map_monoE`, `cvg_fmap`, `continuous_cvg`, `continuous_is_cvg`,
+	  `continuous2_cvg`, `cvg_near_cst`, `is_cvg_near_cst`, `cvg_cst`, `is_cvg_cst`,
+	  `fmap_within_eq`, `cvg_image`, `cvg_fmap2`, `cvg_within_filter`, `cvg_app_within`,
+	  `meets_openr`, `meets_openl`, `meetsxx`, `proper_meetsxx`, `ultra_cvg_clusterE`,
+	  `ultraFilterLemma`, `compact_ultra`, `proper_image`, `in_ultra_setVsetC`,
+	  `ultra_image`, `filter_finI`, `close_cvg`, `discrete_cvg`, `nbhs_E`, `cvg_closeP`,
+	  `cvg_mx_entourageP`, `cvg_fct_entourageP`, `fcvg_ball2P`, `cvg_ball2P`, `cauchy_cvgP`,
+	  `mx_complete`, `Uniform_isComplete.Build`, `cauchy_ballP`, `cauchy_exP`, `cauchyP`,
+      `compact_cauchy_cvg`, `pointwise_cvgE`, `pointwise_uniform_cvg`, `cvg_sigL`, `uniform_restrict_cvg`,
+	  `cvg_uniformU`, `cvg_uniform_set0`, `fam_cvgP`, `family_cvg_subset`,
+	  `family_cvg_finite_covers`, `fam_cvgE`, `Nbhs_isTopological`, `compact_open_fam_compactP`,
+      `compact_cvg_within_compact`, `nbhs_subspace`, `subspace_cvgP`, `uniform_limit_continuous`,
+	  `uniform_limit_continuous_subspace`, `pointwise_compact_cvg`
+	* `t` in module type `PropInFilterSig`
+  + canonical `matrix_filtered` -> instance using `isFiltered.Build`
+  + now use `nbhs` instead of `[filter of ...]`
+    * notations `-->`, `E @[ x --> F ]`, `f @ F`, ```E `@[ x --> F ]```, ```f `@ G```,
+	  `{ptws, F --> f }`
+  + notation `lim` is now a definition
+  + canonical `filtered_prod` -> instances using `isFiltered.Build`, `selfFiltered.Build`
+  + now use `set_system` and also `nbhsType` instead of `filteredType ...`
+    * lemmas `cvg_ex`, `cvgP`, `cvg_toP`, `dvgP`, `cvgNpoint`, `eq_is_cvg`
+  + canonicals `filter_on_eqType`, `filter_on_choiceType`, `filter_on_PointedType`,
+    `filter_on_FilteredType` -> instances using `gen_eqMixin`, `gen_choiceMixin`,
+	`isPointed.Build`, `isFiltered.Build`
+  + canonical `bool_discrete_filter` -> instance using `hasNbhs.Build`
+  + module `Topological` (packed class) -> mixin `Nbhs_isTopological`,
+    structure `Topological`, type `topologicalType`
+	* definition `open` now a field of the mixin
+  + notation `continuous` now uses definition `continuous_at`
+  + section `TopologyOfFilter` -> factory `Nbhs_isNbhsTopological`
+  + section `TopologyOfOpen` -> factory `Pointed_isOpenTopological`
+  + section `TopologyOfBase` -> factory `Pointed_isBaseTopological`
+  + section `TopologyOfSubbase` -> factory `Pointed_isSubBaseTopological`
+  + definition `Pointed_isSubBaseTopological`,
+    canonicals `nat_filteredType`, `nat_topologicalType` ->
+	instance using `Pointed_isBaseTopological.Build`
+  + filter now explicit in the notation `X --> Y`
+    * lemmas `cvg_addnr`, `cvg_subnr`, `cvg_mulnl`, `cvg_mulnr`, `cvg_divnr`
+  + definition `prod_topologicalTypeMixin`, canonical `prod_topologicalType` ->
+    instances using `hasNbhs.Build`, `Nbhs_isNbhsTopological.Build`
+  + definition `matrix_topologicalTypeMixin`, canonical `matrix_topologicalType` ->
+    instance using `Nbhs_isNbhsTopological.Build`
+  + definitions `weak_topologicalTypeMixin`, `weak_topologicalType` ->
+    instances using `Pointed.on`, `Pointed_isOpenTopological.Build`
+  + definitions `sup_topologicalTypeMixin`, `sup_topologicalType` ->
+    instances using `Pointed.on` and `Pointed_isSubBaseTopological.Build`
+  + definition `product_topologicalType` -> definition `product_topology_def`
+    and instance using `Topological.copy`
+  + in `lim_id`: `nbhs` now explicit
+  + canonical `bool_discrete_topology` -> instance using `bool_discrete_topology`
+  + module `Uniform` (packed class) -> mixin `Nbhs_isUniform_mixin`,
+    structure `Uniform`, type `uniformType`,
+    factories `Nbhs_isUniform`, `isUniform`
+  + definition `prod_uniformType_mixin`, canonical `prod_uniformType` ->
+    instance using `Nbhs_isUniform.Build`
+  + definition `matrix_uniformType_mixin`, canonical `matrix_uniformType` ->
+    instance using `Nbhs_isUniform.Build`
+  + definitions `weak_uniform_mixin`, `weak_uniformType` -> instance
+    using `Nbhs_isUniform.Build`
+  + definitions `fct_uniformType_mixin`, `fct_topologicalTypeMixin`,
+    `generic_source_filter`, `fct_topologicalType`, `fct_uniformType` ->
+	definition `arrow_uniform` and instance using `arrow_uniform`
+  + definitions `sup_uniform_mixin`, `sup_uniformType` -> instance using
+    `Nbhs_isUniform.Build`
+  + definition `product_uniformType` -> instance using `Uniform.copy`
+  + definition `discrete_uniformType` -> instance using `Choice.on`,
+    `Choice.on`, `discrete_uniform_mixin`
+  + module `PseudoMetric` (packed class) -> factory `Nbhs_isPseudoMetric`
+  + definition `ball` now a field of factory `Nbhs_isPseudoMetric`
+  + definition `matrix_pseudoMetricType_mixin`, canonical `matrix_pseudoMetricType` ->
+    instance using `Uniform_isPseudoMetric.Build`
+  + definition `prod_pseudoMetricType_mixin`, canonical `prod_pseudoMetricType` ->
+    instance using `Uniform_isPseudoMetric.Build`
+  + definition `fct_pseudoMetricType_mixin`, canonical `fct_pseudoMetricType` ->
+    instance using `Uniform_isPseudoMetric.Build`
+  + canonical `quotient_subtype` -> instance using `Quotient.copy`
+  + canonical `quotient_eq` -> instance using `[Sub ... of ... by %/]`
+  + canonical `quotient_choice` -> instance using `[Choice of ... by <:]`
+  + canonical `quotient_pointed` -> instance using `isPointed.Build`
+  + in definition `quotient_topologicalType_mixin`:
+    `topologyOfOpenMixin` -> `Pointed_isOpenTopological.Build`
+  + canonical `quotient_topologicalType` -> instance using `quotient_topologicalType_mixin`
+  + lemma `repr_comp_continuous` uses the notation `\pi_` instead of `... == ... %[mod ...]`
+  + definition `discrete_pseudoMetricType` -> instead using `discrete_pseudometric_mixin`
+  + module `Complete` (packed class) -> mixin `Uniform_isComplete`,
+    structure `Complete`, type `completeType`
+	  * lemma `cauchy_cvg` now a mixin field
+  + canonical `matrix_completeType` -> instance using `Uniform_isComplete.Build`
+  + canonical `fun_completeType` -> instance using `Uniform_isComplete.Build`
+  + module `CompletePseudoMetric` (packed class) -> structure `CompletePseudoMetric`
+  + matrix instance using `Uniform_isComplete.Build`
+  + function instance using `Uniform_isComplete.Build`
+  + module `regular_topology` -> instances using ` Pointed.on`,
+    `hasNbhs.Build`, `Nbhs_isPseudoMetric.Build`
+  + in module `numFieldTopology`:
+    * `realType`, `rcfType`, `archiFieldType`, `realFieldType`, `numClosedFieldType`,
+	  `numFieldType` instances using `PseudoMetric.copy`
+  + definition `fct_RestrictedUniform`, `fct_RestrictedUniformTopology`, canonical
+    `fct_RestrictUniformFilteredType`, `fct_RestrictUniformTopologicalType`, `fct_restrictedUniformType`
+    ->
+    definition `uniform_fun`, instance using `Unifom.copy` for ```{uniform` _ -> _}```
+  + definitions `fct_Pointwise`, `fct_PointwiseTopology`, canonicals `fct_PointwiseFilteredType`,
+    `fct_PointwiseTopologicalType` -> definition `pointwise_fun`, instance using `Topological.copy`
+  + definition `compact_openK_topological_mixin`, canonical `compact_openK_filter`,
+    `compact_openK_topological` -> instances using `Pointed.on`,
+    `hasNbhs.Build`, `compact_openK_openE_subproof` for `compact_openK`
+  + canonical `compact_open_pointedType`, definition `compact_open_topologicalType`,
+    canonicals `compact_open_filtered`, `compact_open_filtered` -> definition `compact_open_def`,
+	instances using `Pointed.on`, `Nbhs.copy`, `Pointed.on`, `Nbhs_isTopological`
+  + definitions `weak_pseudoMetricType_mixin`, `weak_pseudoMetricType` -> lemmas
+    `weak_pseudo_metric_ball_center`, `weak_pseudo_metric_entourageE`, instance using `niform_isPseudoMetric.Build`
+  + definition `countable_uniform_pseudoMetricType_mixin` -> module `countable_uniform`
+    with definition `type`, instances using `Uniform.on`, `Uniform_isPseudoMetric.Build`,
+	lemma `countable_uniform_bounded`, notation `countable_uniform`
+  + definitions `sup_pseudoMetric_mixin`, `sup_pseudoMetricType`, `product_pseudoMetricType` ->
+    instances using `PseudoMetric.on`, `PseudoMetric.copy`
+  + definitions `subspace_pointedType`, `subspace_topologicalMixin`, canonicals `subspace_filteredType`,
+    `subspace_topologicalType` -> instance using `Choice.copy`, `isPointed.Build`, `hasNbhs.Build`,
+	lemmas `nbhs_subspaceP_subproof`, `nbhs_subspace_singleton`, `nbhs_subspace_nbhs`, instance using
+	`Nbhs_isNbhsTopological.Build`
+  + definition `subspace_uniformMixin`, canonical `subspace_uniformType` -> instance using
+    `Nbhs_isUniform_mixin.Build`
+  + definition `subspace_pseudoMetricType_mixin`, canonical `subspace_pseudoMetricType` -> lemmas `subspace_pm_ball_center`,
+    `subspace_pm_ball_sym`, `subspace_pm_ball_triangle`, `subspace_pm_entourageE`, instance using
+    `Uniform_isPseudoMetric.Build`
+  + section `gauges` -> module `gauge`
+    * `gauge_pseudoMetricType` -> `gauge.type` (instances using `Uniform.on`, `PseudoMetric.on`)
+	* `gauge_uniformType` -> `gauge.type`
+
 ### Renamed
 
 ### Generalized
@@ -382,6 +560,14 @@
   + in definition `cantor_space`: `product_uniformType` -> `prod_topology`
 	* instances using `Pointed.on`, `Nbhs.on`, `Topological.on`
 
+- in `topology.v`:
+  + now use `nbhsType` instead of `topologicalType`
+    * lemma `near_fun`
+    * definition `discrete_space`
+    * definition `discrete_uniform_mixin`
+	* definition `discrete_ball`, lemma `discrete_ball_center`,
+	  definition `discrete_pseudometric_mixin`
+
 ### Deprecated
 
 ### Removed
@@ -450,6 +636,19 @@
   + canonical `matrix_normedZmodType`
   + lemmas `eq_cvg`, `eq_is_cvg`
 
+- in `topology.v`:
+  + structure `source`, definition `source_filter`
+  + definition `filter_of`, notation `[filter of ...]` (now replaced by `nbhs`), lemma `filter_of_filterE`
+  + definition `open_of_nbhs`
+  + definition `open_from`, lemma `open_fromT`
+  + canonical `eventually_filter_source`
+  + canonical `discrete_topological_mixin`
+  + canonical `set_filter_source`
+  + definitions `filtered_of_normedZmod`, `pseudoMetric_of_normedDomain`
+  + definitions `fct_UniformFamily` (use `uniform_fun_family` instead), canonicals `fct_UniformFamilyFilteredType`,
+   `fct_UniformFamilyTopologicalType`, `fct_UniformFamilyUniformType`
+
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/topology.v b/theories/topology.v
@@ -2116,7 +2116,7 @@ HB.end.
 
 (** Topology defined by open sets *)
 
-Definition nbhs_of_open (T : pointedType) (op : set T -> Prop) (p : T) (A : set T) :=
+Definition nbhs_of_open (T : Type) (op : set T -> Prop) (p : T) (A : set T) :=
   exists B, [/\ op B, B p & B `<=` A].
 
 (* was topologyOfOpenMixin *)
@@ -2384,7 +2384,6 @@ HB.instance Definition _ := Pointed_isBaseTopological.Build nat bT bD.
 
 End nat_topologicalType.
 
-
 Global Instance eventually_filter : ProperFilter eventually.
 Proof.
 eapply @filter_from_proper; last by move=> i _; exists i => /=.
@@ -5894,7 +5893,7 @@ HB.instance Definition _ (U : Type) (V : topologicalType) :=
 End PtwsFun.
 
 Lemma pointwise_cvgE {U : Type} {V : topologicalType}
-    (F : set_system(U -> V)) (A : set U) (f : U -> V) :
+    (F : set_system (U -> V)) (A : set U) (f : U -> V) :
   {ptws, F --> f} = (F --> (f : {ptws U -> V})).
 Proof. by []. Qed.