From 2e448c5dbb49efdd7ab6066084f9c1d75c74b5c6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 10 Jan 2025 22:57:04 +0900 Subject: [PATCH] doc, trailing spaces --- CHANGELOG_UNRELEASED.md | 114 +------------------ theories/topology_theory/discrete_topology.v | 68 +++++++---- 2 files changed, 47 insertions(+), 135 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e319ca1fa..115de956b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,105 +14,6 @@ + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, `derivable_horner`, `derivE`, `continuous_horner` + instance `is_derive_poly` -- in file `separation_axioms.v`, - + new lemmas `compact_normal_local`, and `compact_normal`. - -- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals` - with files - + `xfinmap.v` - + `discrete.v` - + `realseq.v` - + `realsum.v` - + `distr.v` - -- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals` - with file - + `Rstruct.v` - -- package `coq-mathcomp-analysis-stdlib` depending on - `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files - + `Rstruct_topology.v` - + `showcase/uniform_bigO.v` - -- in file `separation_axioms.v`, - + new lemmas `compact_normal_local`, and `compact_normal`. - -- in file `topology_theory/one_point_compactification.v`, - + new definitions `one_point_compactification`, and `one_point_nbhs`. - + new lemmas `one_point_compactification_compact`, - `one_point_compactification_some_nbhs`, - `one_point_compactification_some_continuous`, - `one_point_compactification_open_some`, - `one_point_compactification_weak_topology`, and - `one_point_compactification_hausdorff`. - -- in file `normedtype.v`, - + new definition `type` (in module `completely_regular_uniformity`) - + new lemmas `normal_completely_regular`, - `one_point_compactification_completely_reg`, - `nbhs_one_point_compactification_weakE`, - `locally_compact_completely_regular`, and - `completely_regular_regular`. - + new lemmas `near_in_itvoy`, `near_in_itvNyo` - -- in file `mathcomp_extra.v`, - + new definition `sigT_fun`. -- in file `sigT_topology.v`, - + new definition `sigT_nbhs`. - + new lemmas `sigT_nbhsE`, `existT_continuous`, `existT_open_map`, - `existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and - `sigT_compact`. -- in file `separation_axioms.v`, - + new lemma `sigT_hausdorff`. - -- in `measure.v`: - + lemma `countable_measurable` -- in `realfun.v`: - + lemma `cvgr_dnbhsP` - + new definitions `prodA`, and `prodAr`. - + new lemmas `prodAK`, `prodArK`, and `swapK`. -- in file `product_topology.v`, - + new lemmas `swap_continuous`, `prodA_continuous`, and - `prodAr_continuous`. - -- file `homotopy_theory/homotopy.v` -- file `homotopy_theory/wedge_sigT.v` -- in file `homotopy_theory/wedge_sigT.v` - + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`. - + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`, - `wedge_liftE`, `wedge_openP`, - `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, - `wedge_compact`, `wedge_connected`. - -- in `boolp.`: - + lemma `existT_inj` -- in file `order_topology.v` - + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and - `max_fun_continuous`. - -- in file `bool_topology.v`, - + new lemma `bool_compact`. - -### Changed - -- in file `normedtype.v`, - changed `completely_regular_space` to depend on uniform separators - which removes the dependency on `R`. The old formulation can be - recovered easily with `uniform_separatorP`. - -- moved from `Rstruct.v` to `Rstruct_topology.v` - + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, - `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs` - and `nbhs_pt_comp` - -- moved from `real_interval.v` to `normedtype.v` - + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`, - `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`, - `disj_itv_Rhull` -- in `topology.v`: - + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, - `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned - into local `Let`'s - in `lebesgue_integral.v`: + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` @@ -129,6 +30,9 @@ - in `classical_sets.v`: + lemmas `xsectionE`, `ysectionE` +- in file `bool_topology.v`, + + new lemma `bool_compact`. + ### Changed - in `lebesgue_integrale.v` @@ -142,12 +46,12 @@ - moved from `lebesgue_integral.v` to `measure.v` and generalized + lemmas `measurable_xsection`, `measurable_ysection` + - moved from `topology_structure.v` to `discrete_topology.v`: `discrete_open`, `discrete_set1`, `discrete_closed`, and `discrete_cvg`. - moved from `pseudometric_structure.v` to `discrete_topology.v`: `discrete_ent`, `discrete_ball`, and `discrete_topology`. - - in file `cantor.v`, `cantor_space` now defined in terms of `bool`. - in file `separation_axioms.v`, updated `discrete_hausdorff`, and `discrete_zero_dimension` to take a `discreteTopologicalType`. @@ -184,17 +88,7 @@ - in `sequences.v`: + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`, `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0) -- in `lebesgue_integral.v`: - + definition `cst_mfun` - + lemma `mfun_cst` - -- in `cardinality.v`: - + lemma `cst_fimfun_subproof` -- in `lebesgue_integral.v`: - + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead) - + lemma `cst_nnfun_subproof` (turned into a `Let`) - + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) - in file `topology_structure.v`, removed `discrete_sing`, `discrete_nbhs`, and `discrete_space`. - in file `nat_topology.v`, removed `discrete_nat`. - in file `pseudometric_structure.v`, removed `discrete_ball_center`, `discrete_topology_type`, and diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v index 94e837eb8..0a4838b12 100644 --- a/theories/topology_theory/discrete_topology.v +++ b/theories/topology_theory/discrete_topology.v @@ -3,12 +3,30 @@ From mathcomp Require Import all_ssreflect all_algebra all_classical all_reals. From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import order_topology pseudometric_structure compact. +(**md**************************************************************************) +(* # Discrete Topology *) +(* ``` *) +(* discreteNbhsType == neighborhoods are principal filters *) +(* discrete_ent == entourages of the discrete uniformity *) +(* topology, equipped with the Uniform *) +(* structure *) +(* discrete_ball == singleton balls for the discrete metric, *) +(* equipped with the Uniform structure *) +(* discreteTopologicalType == types with a discrete topology *) +(* discreteOrderTopologicalType == *) +(* pdiscreteTopologicalType == *) +(* pdiscreteOrderTopologicalType == *) +(* discreteUniformType == *) +(* discretePseudoMetricType == *) +(* discrete_topology T == alias attaching discrete structures for *) +(* topology, uniformity, and pseudometric *) +(* ``` *) +(******************************************************************************) Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope classical_set_scope. Local Open Scope ring_scope. - HB.mixin Record Discrete_ofNbhs T of Nbhs T := { nbhs_principalE : (@nbhs T _) = principal_filter; }. @@ -16,45 +34,45 @@ HB.mixin Record Discrete_ofNbhs T of Nbhs T := { #[short(type="discreteNbhsType")] HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}. - Definition discrete_ent {T} : set (set (T * T)) := globally (range (fun x => (x, x))). -(** Note: having the discrete topology does not guarantee the discrete +(** Note: having the discrete topology does not guarantee the discrete uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *) HB.mixin Record Discrete_ofUniform T of Uniform T := { uniform_discrete : @entourage T = discrete_ent }. -Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := x = y. +Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := + x = y. -HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of +HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of PseudoMetric R T := { metric_discrete : @ball R T = @discrete_ball R T }. #[short(type="discreteTopologicalType")] -HB.structure Definition DiscreteTopology := +HB.structure Definition DiscreteTopology := { T of DiscreteNbhs T & Topological T}. #[short(type="discreteOrderTopologicalType")] -HB.structure Definition DiscreteOrderTopology d := +HB.structure Definition DiscreteOrderTopology d := { T of Discrete_ofNbhs T & OrderTopological d T}. #[short(type="pdiscreteTopologicalType")] -HB.structure Definition PointedDiscreteTopology := +HB.structure Definition PointedDiscreteTopology := { T of DiscreteTopology T & Pointed T}. #[short(type="pdiscreteOrderTopologicalType")] -HB.structure Definition PointedDiscreteOrderTopology d := +HB.structure Definition PointedDiscreteOrderTopology d := { T of Discrete_ofNbhs T & OrderTopological d T & Pointed T}. #[short(type="discreteUniformType")] -HB.structure Definition DiscreteUniform := +HB.structure Definition DiscreteUniform := { T of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}. #[short(type="discretePseudoMetricType")] -HB.structure Definition DiscretePseudoMetric {R : numDomainType} := +HB.structure Definition DiscretePseudoMetric {R : numDomainType} := { T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}. HB.builders Context T of Discrete_ofNbhs T. @@ -65,7 +83,8 @@ Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed. Local Lemma principal_nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p. Proof. by rewrite nbhs_principalE => /principal_filterP. Qed. -Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : nbhs p A -> nbhs p (nbhs^~ A). +Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : + nbhs p A -> nbhs p (nbhs^~ A). Proof. by move=> ?; rewrite {1}nbhs_principalE; apply/principal_filterP. Qed. HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T @@ -101,16 +120,16 @@ Qed. Local Lemma discrete_entourage_nbhsE : (@nbhs T _) = nbhs_ d. Proof. rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U. - move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-]. + move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-]. by move=> z /= /set_mem; rewrite /diagonal /= => <-. case => w entW wU; apply/principal_filterP; apply: wU; apply/mem_set. exact: entW. Qed. HB.instance Definition _ := @Nbhs_isUniform.Build T - discrete_ent - discrete_entourage_filter - discrete_entourage_diagonal + discrete_ent + discrete_entourage_filter + discrete_entourage_diagonal discrete_entourage_inv discrete_entourage_split_ex discrete_entourage_nbhsE. @@ -119,12 +138,12 @@ HB.instance Definition _ := @Discrete_ofUniform.Build T erefl. HB.end. -HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of +HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of DiscreteUniform T := {}. HB.builders Context R T of DiscretePseudoMetric_ofUniform R T. -Local Lemma discrete_ball_center x (eps : R) : 0 < eps -> +Local Lemma discrete_ball_center x (eps : R) : 0 < eps -> @discrete_ball R T x eps x. Proof. by []. Qed. @@ -143,9 +162,9 @@ move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //. by rewrite {2}z12 -surjective_pairing. Qed. -HB.instance Definition _ := - @Uniform_isPseudoMetric.Build R T (@discrete_ball R T) - discrete_ball_center discrete_ball_sym discrete_ball_triangle +HB.instance Definition _ := + @Uniform_isPseudoMetric.Build R T (@discrete_ball R T) + discrete_ball_center discrete_ball_sym discrete_ball_triangle discrete_entourageE. Local Lemma discrete_ballE : @ball R T = @discrete_ball R T. @@ -155,9 +174,8 @@ HB.instance Definition _ := @Discrete_ofPseudometric.Build R T discrete_ballE. HB.end. -(** we introducing an alias attaching discrete structures for - topology, uniformity, and pseudometric *) Definition discrete_topology (T : Type) : Type := T. + HB.instance Definition _ (T : choiceType) := Choice.copy (discrete_topology T) T. HB.instance Definition _ (T : pointedType) := @@ -166,9 +184,9 @@ HB.instance Definition _ (T : choiceType) := hasNbhs.Build (discrete_topology T) principal_filter. HB.instance Definition _ (T : choiceType) := Discrete_ofNbhs.Build (discrete_topology T) erefl. -HB.instance Definition _ (T : choiceType) := +HB.instance Definition _ (T : choiceType) := DiscreteUniform_ofNbhs.Build (discrete_topology T). -HB.instance Definition _ {R : numDomainType} (T : choiceType) := +HB.instance Definition _ {R : numDomainType} (T : choiceType) := @DiscretePseudoMetric_ofUniform.Build R (discrete_topology T). Section discrete_topology.