Skip to content

Commit 2e448c5

Browse files
affeldt-aistaffeldt-aist
committed
doc, trailing spaces
1 parent 7346645 commit 2e448c5

File tree

2 files changed

+47
-135
lines changed

2 files changed

+47
-135
lines changed

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 4 additions & 110 deletions
Original file line numberDiff line numberDiff line change
@@ -14,105 +14,6 @@
1414
+ lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`,
1515
`derivable_horner`, `derivE`, `continuous_horner`
1616
+ instance `is_derive_poly`
17-
- in file `separation_axioms.v`,
18-
+ new lemmas `compact_normal_local`, and `compact_normal`.
19-
20-
- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals`
21-
with files
22-
+ `xfinmap.v`
23-
+ `discrete.v`
24-
+ `realseq.v`
25-
+ `realsum.v`
26-
+ `distr.v`
27-
28-
- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals`
29-
with file
30-
+ `Rstruct.v`
31-
32-
- package `coq-mathcomp-analysis-stdlib` depending on
33-
`coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files
34-
+ `Rstruct_topology.v`
35-
+ `showcase/uniform_bigO.v`
36-
37-
- in file `separation_axioms.v`,
38-
+ new lemmas `compact_normal_local`, and `compact_normal`.
39-
40-
- in file `topology_theory/one_point_compactification.v`,
41-
+ new definitions `one_point_compactification`, and `one_point_nbhs`.
42-
+ new lemmas `one_point_compactification_compact`,
43-
`one_point_compactification_some_nbhs`,
44-
`one_point_compactification_some_continuous`,
45-
`one_point_compactification_open_some`,
46-
`one_point_compactification_weak_topology`, and
47-
`one_point_compactification_hausdorff`.
48-
49-
- in file `normedtype.v`,
50-
+ new definition `type` (in module `completely_regular_uniformity`)
51-
+ new lemmas `normal_completely_regular`,
52-
`one_point_compactification_completely_reg`,
53-
`nbhs_one_point_compactification_weakE`,
54-
`locally_compact_completely_regular`, and
55-
`completely_regular_regular`.
56-
+ new lemmas `near_in_itvoy`, `near_in_itvNyo`
57-
58-
- in file `mathcomp_extra.v`,
59-
+ new definition `sigT_fun`.
60-
- in file `sigT_topology.v`,
61-
+ new definition `sigT_nbhs`.
62-
+ new lemmas `sigT_nbhsE`, `existT_continuous`, `existT_open_map`,
63-
`existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and
64-
`sigT_compact`.
65-
- in file `separation_axioms.v`,
66-
+ new lemma `sigT_hausdorff`.
67-
68-
- in `measure.v`:
69-
+ lemma `countable_measurable`
70-
- in `realfun.v`:
71-
+ lemma `cvgr_dnbhsP`
72-
+ new definitions `prodA`, and `prodAr`.
73-
+ new lemmas `prodAK`, `prodArK`, and `swapK`.
74-
- in file `product_topology.v`,
75-
+ new lemmas `swap_continuous`, `prodA_continuous`, and
76-
`prodAr_continuous`.
77-
78-
- file `homotopy_theory/homotopy.v`
79-
- file `homotopy_theory/wedge_sigT.v`
80-
- in file `homotopy_theory/wedge_sigT.v`
81-
+ new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`.
82-
+ new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`,
83-
`wedge_liftE`, `wedge_openP`,
84-
`wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`,
85-
`wedge_compact`, `wedge_connected`.
86-
87-
- in `boolp.`:
88-
+ lemma `existT_inj`
89-
- in file `order_topology.v`
90-
+ new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
91-
`max_fun_continuous`.
92-
93-
- in file `bool_topology.v`,
94-
+ new lemma `bool_compact`.
95-
96-
### Changed
97-
98-
- in file `normedtype.v`,
99-
changed `completely_regular_space` to depend on uniform separators
100-
which removes the dependency on `R`. The old formulation can be
101-
recovered easily with `uniform_separatorP`.
102-
103-
- moved from `Rstruct.v` to `Rstruct_topology.v`
104-
+ lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`,
105-
`continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs`
106-
and `nbhs_pt_comp`
107-
108-
- moved from `real_interval.v` to `normedtype.v`
109-
+ lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
110-
`Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
111-
`disj_itv_Rhull`
112-
- in `topology.v`:
113-
+ lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
114-
`subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
115-
into local `Let`'s
11617

11718
- in `lebesgue_integral.v`:
11819
+ lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral`
@@ -129,6 +30,9 @@
12930
- in `classical_sets.v`:
13031
+ lemmas `xsectionE`, `ysectionE`
13132

33+
- in file `bool_topology.v`,
34+
+ new lemma `bool_compact`.
35+
13236
### Changed
13337

13438
- in `lebesgue_integrale.v`
@@ -142,12 +46,12 @@
14246

14347
- moved from `lebesgue_integral.v` to `measure.v` and generalized
14448
+ lemmas `measurable_xsection`, `measurable_ysection`
49+
14550
- moved from `topology_structure.v` to `discrete_topology.v`:
14651
`discrete_open`, `discrete_set1`, `discrete_closed`, and `discrete_cvg`.
14752

14853
- moved from `pseudometric_structure.v` to `discrete_topology.v`:
14954
`discrete_ent`, `discrete_ball`, and `discrete_topology`.
150-
15155
- in file `cantor.v`, `cantor_space` now defined in terms of `bool`.
15256
- in file `separation_axioms.v`, updated `discrete_hausdorff`, and
15357
`discrete_zero_dimension` to take a `discreteTopologicalType`.
@@ -184,17 +88,7 @@
18488
- in `sequences.v`:
18589
+ notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
18690
`ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
187-
- in `lebesgue_integral.v`:
188-
+ definition `cst_mfun`
189-
+ lemma `mfun_cst`
190-
191-
- in `cardinality.v`:
192-
+ lemma `cst_fimfun_subproof`
19391

194-
- in `lebesgue_integral.v`:
195-
+ lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
196-
+ lemma `cst_nnfun_subproof` (turned into a `Let`)
197-
+ lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
19892
- in file `topology_structure.v`, removed `discrete_sing`, `discrete_nbhs`, and `discrete_space`.
19993
- in file `nat_topology.v`, removed `discrete_nat`.
20094
- in file `pseudometric_structure.v`, removed `discrete_ball_center`, `discrete_topology_type`, and

‎theories/topology_theory/discrete_topology.v‎

Lines changed: 43 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -3,58 +3,76 @@ From mathcomp Require Import all_ssreflect all_algebra all_classical all_reals.
33
From mathcomp Require Import topology_structure uniform_structure.
44
From mathcomp Require Import order_topology pseudometric_structure compact.
55

6+
(**md**************************************************************************)
7+
(* # Discrete Topology *)
8+
(* ``` *)
9+
(* discreteNbhsType == neighborhoods are principal filters *)
10+
(* discrete_ent == entourages of the discrete uniformity *)
11+
(* topology, equipped with the Uniform *)
12+
(* structure *)
13+
(* discrete_ball == singleton balls for the discrete metric, *)
14+
(* equipped with the Uniform structure *)
15+
(* discreteTopologicalType == types with a discrete topology *)
16+
(* discreteOrderTopologicalType == *)
17+
(* pdiscreteTopologicalType == *)
18+
(* pdiscreteOrderTopologicalType == *)
19+
(* discreteUniformType == *)
20+
(* discretePseudoMetricType == *)
21+
(* discrete_topology T == alias attaching discrete structures for *)
22+
(* topology, uniformity, and pseudometric *)
23+
(* ``` *)
24+
(******************************************************************************)
625
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
726

827
Local Open Scope classical_set_scope.
928
Local Open Scope ring_scope.
1029

11-
1230
HB.mixin Record Discrete_ofNbhs T of Nbhs T := {
1331
nbhs_principalE : (@nbhs T _) = principal_filter;
1432
}.
1533

1634
#[short(type="discreteNbhsType")]
1735
HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}.
1836

19-
2037
Definition discrete_ent {T} : set (set (T * T)) :=
2138
globally (range (fun x => (x, x))).
2239

23-
(** Note: having the discrete topology does not guarantee the discrete
40+
(** Note: having the discrete topology does not guarantee the discrete
2441
uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *)
2542
HB.mixin Record Discrete_ofUniform T of Uniform T := {
2643
uniform_discrete : @entourage T = discrete_ent
2744
}.
2845

29-
Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := x = y.
46+
Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop :=
47+
x = y.
3048

31-
HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of
49+
HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of
3250
PseudoMetric R T := {
3351
metric_discrete : @ball R T = @discrete_ball R T
3452
}.
3553

3654
#[short(type="discreteTopologicalType")]
37-
HB.structure Definition DiscreteTopology :=
55+
HB.structure Definition DiscreteTopology :=
3856
{ T of DiscreteNbhs T & Topological T}.
3957

4058
#[short(type="discreteOrderTopologicalType")]
41-
HB.structure Definition DiscreteOrderTopology d :=
59+
HB.structure Definition DiscreteOrderTopology d :=
4260
{ T of Discrete_ofNbhs T & OrderTopological d T}.
4361

4462
#[short(type="pdiscreteTopologicalType")]
45-
HB.structure Definition PointedDiscreteTopology :=
63+
HB.structure Definition PointedDiscreteTopology :=
4664
{ T of DiscreteTopology T & Pointed T}.
4765

4866
#[short(type="pdiscreteOrderTopologicalType")]
49-
HB.structure Definition PointedDiscreteOrderTopology d :=
67+
HB.structure Definition PointedDiscreteOrderTopology d :=
5068
{ T of Discrete_ofNbhs T & OrderTopological d T & Pointed T}.
5169

5270
#[short(type="discreteUniformType")]
53-
HB.structure Definition DiscreteUniform :=
71+
HB.structure Definition DiscreteUniform :=
5472
{ T of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}.
5573

5674
#[short(type="discretePseudoMetricType")]
57-
HB.structure Definition DiscretePseudoMetric {R : numDomainType} :=
75+
HB.structure Definition DiscretePseudoMetric {R : numDomainType} :=
5876
{ T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}.
5977

6078
HB.builders Context T of Discrete_ofNbhs T.
@@ -65,7 +83,8 @@ Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed.
6583
Local Lemma principal_nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p.
6684
Proof. by rewrite nbhs_principalE => /principal_filterP. Qed.
6785

68-
Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : nbhs p A -> nbhs p (nbhs^~ A).
86+
Local Lemma principal_nbhs_nbhs (p : T) (A : set T) :
87+
nbhs p A -> nbhs p (nbhs^~ A).
6988
Proof. by move=> ?; rewrite {1}nbhs_principalE; apply/principal_filterP. Qed.
7089

7190
HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T
@@ -101,16 +120,16 @@ Qed.
101120
Local Lemma discrete_entourage_nbhsE : (@nbhs T _) = nbhs_ d.
102121
Proof.
103122
rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U.
104-
move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-].
123+
move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-].
105124
by move=> z /= /set_mem; rewrite /diagonal /= => <-.
106125
case => w entW wU; apply/principal_filterP; apply: wU; apply/mem_set.
107126
exact: entW.
108127
Qed.
109128

110129
HB.instance Definition _ := @Nbhs_isUniform.Build T
111-
discrete_ent
112-
discrete_entourage_filter
113-
discrete_entourage_diagonal
130+
discrete_ent
131+
discrete_entourage_filter
132+
discrete_entourage_diagonal
114133
discrete_entourage_inv
115134
discrete_entourage_split_ex
116135
discrete_entourage_nbhsE.
@@ -119,12 +138,12 @@ HB.instance Definition _ := @Discrete_ofUniform.Build T erefl.
119138

120139
HB.end.
121140

122-
HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of
141+
HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of
123142
DiscreteUniform T := {}.
124143

125144
HB.builders Context R T of DiscretePseudoMetric_ofUniform R T.
126145

127-
Local Lemma discrete_ball_center x (eps : R) : 0 < eps ->
146+
Local Lemma discrete_ball_center x (eps : R) : 0 < eps ->
128147
@discrete_ball R T x eps x.
129148
Proof. by []. Qed.
130149

@@ -143,9 +162,9 @@ move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //.
143162
by rewrite {2}z12 -surjective_pairing.
144163
Qed.
145164

146-
HB.instance Definition _ :=
147-
@Uniform_isPseudoMetric.Build R T (@discrete_ball R T)
148-
discrete_ball_center discrete_ball_sym discrete_ball_triangle
165+
HB.instance Definition _ :=
166+
@Uniform_isPseudoMetric.Build R T (@discrete_ball R T)
167+
discrete_ball_center discrete_ball_sym discrete_ball_triangle
149168
discrete_entourageE.
150169

151170
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.
155174

156175
HB.end.
157176

158-
(** we introducing an alias attaching discrete structures for
159-
topology, uniformity, and pseudometric *)
160177
Definition discrete_topology (T : Type) : Type := T.
178+
161179
HB.instance Definition _ (T : choiceType) :=
162180
Choice.copy (discrete_topology T) T.
163181
HB.instance Definition _ (T : pointedType) :=
@@ -166,9 +184,9 @@ HB.instance Definition _ (T : choiceType) :=
166184
hasNbhs.Build (discrete_topology T) principal_filter.
167185
HB.instance Definition _ (T : choiceType) :=
168186
Discrete_ofNbhs.Build (discrete_topology T) erefl.
169-
HB.instance Definition _ (T : choiceType) :=
187+
HB.instance Definition _ (T : choiceType) :=
170188
DiscreteUniform_ofNbhs.Build (discrete_topology T).
171-
HB.instance Definition _ {R : numDomainType} (T : choiceType) :=
189+
HB.instance Definition _ {R : numDomainType} (T : choiceType) :=
172190
@DiscretePseudoMetric_ofUniform.Build R (discrete_topology T).
173191

174192
Section discrete_topology.

0 commit comments

Comments
 (0)