Skip to content

Commit 5f47a66

Browse files
affeldt-aistaffeldt-aist
committed
doc, trailing spaces
1 parent 7346645 commit 5f47a66

File tree

2 files changed

+48
-135
lines changed

2 files changed

+48
-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: 44 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -3,58 +3,77 @@ 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 == *)
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 == type of choice types with a discrete *)
16+
(* topology *)
17+
(* discreteOrderTopologicalType == *)
18+
(* pdiscreteTopologicalType == *)
19+
(* pdiscreteOrderTopologicalType == *)
20+
(* discreteUniformType == *)
21+
(* discretePseudoMetricType == *)
22+
(* discrete_topology T == alias attaching discrete structures for *)
23+
(* topology, uniformity, and pseudometric *)
24+
(* ``` *)
25+
(******************************************************************************)
626
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
727

828
Local Open Scope classical_set_scope.
929
Local Open Scope ring_scope.
1030

11-
1231
HB.mixin Record Discrete_ofNbhs T of Nbhs T := {
1332
nbhs_principalE : (@nbhs T _) = principal_filter;
1433
}.
1534

1635
#[short(type="discreteNbhsType")]
1736
HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}.
1837

19-
2038
Definition discrete_ent {T} : set (set (T * T)) :=
2139
globally (range (fun x => (x, x))).
2240

23-
(** Note: having the discrete topology does not guarantee the discrete
41+
(** Note: having the discrete topology does not guarantee the discrete
2442
uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *)
2543
HB.mixin Record Discrete_ofUniform T of Uniform T := {
2644
uniform_discrete : @entourage T = discrete_ent
2745
}.
2846

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

31-
HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of
50+
HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of
3251
PseudoMetric R T := {
3352
metric_discrete : @ball R T = @discrete_ball R T
3453
}.
3554

3655
#[short(type="discreteTopologicalType")]
37-
HB.structure Definition DiscreteTopology :=
56+
HB.structure Definition DiscreteTopology :=
3857
{ T of DiscreteNbhs T & Topological T}.
3958

4059
#[short(type="discreteOrderTopologicalType")]
41-
HB.structure Definition DiscreteOrderTopology d :=
60+
HB.structure Definition DiscreteOrderTopology d :=
4261
{ T of Discrete_ofNbhs T & OrderTopological d T}.
4362

4463
#[short(type="pdiscreteTopologicalType")]
45-
HB.structure Definition PointedDiscreteTopology :=
64+
HB.structure Definition PointedDiscreteTopology :=
4665
{ T of DiscreteTopology T & Pointed T}.
4766

4867
#[short(type="pdiscreteOrderTopologicalType")]
49-
HB.structure Definition PointedDiscreteOrderTopology d :=
68+
HB.structure Definition PointedDiscreteOrderTopology d :=
5069
{ T of Discrete_ofNbhs T & OrderTopological d T & Pointed T}.
5170

5271
#[short(type="discreteUniformType")]
53-
HB.structure Definition DiscreteUniform :=
72+
HB.structure Definition DiscreteUniform :=
5473
{ T of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}.
5574

5675
#[short(type="discretePseudoMetricType")]
57-
HB.structure Definition DiscretePseudoMetric {R : numDomainType} :=
76+
HB.structure Definition DiscretePseudoMetric {R : numDomainType} :=
5877
{ T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}.
5978

6079
HB.builders Context T of Discrete_ofNbhs T.
@@ -65,7 +84,8 @@ Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed.
6584
Local Lemma principal_nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p.
6685
Proof. by rewrite nbhs_principalE => /principal_filterP. Qed.
6786

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

7191
HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T
@@ -101,16 +121,16 @@ Qed.
101121
Local Lemma discrete_entourage_nbhsE : (@nbhs T _) = nbhs_ d.
102122
Proof.
103123
rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U.
104-
move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-].
124+
move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-].
105125
by move=> z /= /set_mem; rewrite /diagonal /= => <-.
106126
case => w entW wU; apply/principal_filterP; apply: wU; apply/mem_set.
107127
exact: entW.
108128
Qed.
109129

110130
HB.instance Definition _ := @Nbhs_isUniform.Build T
111-
discrete_ent
112-
discrete_entourage_filter
113-
discrete_entourage_diagonal
131+
discrete_ent
132+
discrete_entourage_filter
133+
discrete_entourage_diagonal
114134
discrete_entourage_inv
115135
discrete_entourage_split_ex
116136
discrete_entourage_nbhsE.
@@ -119,12 +139,12 @@ HB.instance Definition _ := @Discrete_ofUniform.Build T erefl.
119139

120140
HB.end.
121141

122-
HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of
142+
HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of
123143
DiscreteUniform T := {}.
124144

125145
HB.builders Context R T of DiscretePseudoMetric_ofUniform R T.
126146

127-
Local Lemma discrete_ball_center x (eps : R) : 0 < eps ->
147+
Local Lemma discrete_ball_center x (eps : R) : 0 < eps ->
128148
@discrete_ball R T x eps x.
129149
Proof. by []. Qed.
130150

@@ -143,9 +163,9 @@ move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //.
143163
by rewrite {2}z12 -surjective_pairing.
144164
Qed.
145165

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

151171
Local Lemma discrete_ballE : @ball R T = @discrete_ball R T.
@@ -155,9 +175,8 @@ HB.instance Definition _ := @Discrete_ofPseudometric.Build R T discrete_ballE.
155175

156176
HB.end.
157177

158-
(** we introducing an alias attaching discrete structures for
159-
topology, uniformity, and pseudometric *)
160178
Definition discrete_topology (T : Type) : Type := T.
179+
161180
HB.instance Definition _ (T : choiceType) :=
162181
Choice.copy (discrete_topology T) T.
163182
HB.instance Definition _ (T : pointedType) :=
@@ -166,9 +185,9 @@ HB.instance Definition _ (T : choiceType) :=
166185
hasNbhs.Build (discrete_topology T) principal_filter.
167186
HB.instance Definition _ (T : choiceType) :=
168187
Discrete_ofNbhs.Build (discrete_topology T) erefl.
169-
HB.instance Definition _ (T : choiceType) :=
188+
HB.instance Definition _ (T : choiceType) :=
170189
DiscreteUniform_ofNbhs.Build (discrete_topology T).
171-
HB.instance Definition _ {R : numDomainType} (T : choiceType) :=
190+
HB.instance Definition _ {R : numDomainType} (T : choiceType) :=
172191
@DiscretePseudoMetric_ofUniform.Build R (discrete_topology T).
173192

174193
Section discrete_topology.

0 commit comments

Comments
 (0)