forked from coq-community/topology
-
Notifications
You must be signed in to change notification settings - Fork 0
/
meta.yml
191 lines (139 loc) · 5.35 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
---
fullname: Topology
shortname: topology
organization: coq-community
community: true
action: true
synopsis: General topology in Coq
description: |
This library develops some of the basic concepts
and results of general topology in Coq.
authors:
- name: Daniel Schepler
e-mail: dschepler@gmail.com
initial: true
maintainers:
- name: Andrew Miloradovsky
nickname: amiloradovsky
- name: stop-cran
nickname: stop-cran
- name: Columbus240
nickname: Columbus240
opam-file-maintainer: palmskog@gmail.com
license:
fullname: GNU Lesser General Public License v2.1 or later
identifier: LGPL-2.1-or-later
file: LICENSE
supported_coq_versions:
text: Coq 8.12 or later (use the corresponding branch or release for other Coq versions)
opam: '{(>= "8.12" & < "8.16~") | (= "dev")}'
tested_coq_opam_versions:
- version: dev
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'
dependencies:
- opam:
name: coq-zorns-lemma
version: '{= version}'
description: Zorn's Lemma (set library that is part of this repository)
namespace: Topology
keywords:
- name: topology
- name: filters
- name: nets
- name: metric spaces
- name: real analysis
- name: Urysohn's lemma
- name: Tietze extension theorem
categories:
- name: Mathematics/Real Calculus and Topology
build: |-
## Building and installation instructions
The easiest way to install the latest released version of Topology
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-topology
```
To instead build both Topology and Zorn's Lemma manually, do:
``` shell
git clone https://github.com/coq-community/topology.git
cd topology
make # or make -j <number-of-cores-on-your-machine>
```
documentation: |-
## Contents of Topology, roughly grouped in related categories:
### Basic definitions
- `TopologicalSpaces.v`
- `InteriorsClosures.v`
- `Neighborhoods.v`
- `OpenBases.v`
- `NeighborhoodBases.v`
- `Subbases.v`
- `Continuity.v`
- `Homeomorphisms.v`
### Filters and nets
- `Filters.v`
- `FilterLimits.v`
- `DirectedSets.v`
- `Nets.v`
- `FiltersAndNets.v` - various transformations between filters and nets
### Properties
- `Compactness.v`
- `Connectedness.v`
- `CountabilityAxioms.v` - first countable, second countable, separable, Lindelof
- `SeparatednessAxioms.v` - T0, T1, Hausdorff, etc.
### General constructions of topologies
- `OrderTopology.v`
- `StrongTopology.v` - strong topology induced by a family of maps from
topological spaces
- `WeakTopology.v` - weak topology induced by a family of maps to
topological spaces
- `ProductTopology.v`
- `SumTopology.v` - also called "disjoint union" or "coproduct"
- `SubspaceTopology.v`
- `QuotientTopology.v`
- `ContinuousFactorization.v` - a continuous map factors through its image
### Metric spaces
- `MetricSpaces.v`
- `Completeness.v`
- `Completion.v`
- `UniformTopology.v` - the topology of uniform convergence
### Real analysis
- `SupInf.v`
- `RationalsInReals.v`
- `RTopology.v` - definition and properties of topology on R
- `RFuncContinuity.v` - reproof of continuity of basic functions on R
### "First nontrivial results of topology"
- `UrysohnsLemma.v`
- `TietzeExtension.v`
## Contents of Zorn's Lemma
In alphabetical order, except where related files are grouped together:
- `Cardinals.v` - cardinalities of sets
- `Ordinals.v` - a construction of the ordinals without reference to well-orders
- `Classical_Wf.v` - proofs of the classical equivalence of wellfoundedness, the minimal element property, and the descending sequence property
- `CSB.v` - the Cantor-Schroeder-Bernstein theorem
- `DecidableDec.v` - `classic_dec: forall P: Prop, {P} + {~P}.`
- `DependentTypeChoice.v` - choice on a relation (`forall a: A, B a -> Prop`)
- `EnsemblesImplicit.v` - settings for appropriate implicit parameters for the standard library's Ensembles functions
- `ImageImplicit.v` - same for the standard library's Sets/Image
- `Relation_Definitions_Implicit.v` - same for the standard library's Relation_Definitions
- `EnsemblesSpec.v` - defines a notation for e.g. `[ n: nat | n > 5 /\ even n ] : Ensemble nat.`
- `EnsemblesTactics.v` - defines tactics that help in proofs about Ensembles
- `EnsemblesUtf8.v` - optional UTF-8 notations for set operations
- `Families.v` - operations on families of subsets of `X`, i.e. `Ensemble (Ensemble X)`
- `IndexedFamilies.v` - same for indexed families `A -> Ensemble X`
- `FiniteIntersections.v` - defines the finite intersections of a family of subsets
- `FiniteTypes.v` - definitions and results about finite types
- `CountableTypes.v` - same for countable types
- `InfiniteTypes.v` - same for infinite types
- `FunctionProperties.v` - injective, surjective, etc.
- `InverseImage.v` - inverse images of subsets under functions
- `Powerset_facts.v` - some lemmas about the operations on subsets that the stdlib is missing
- `Proj1SigInjective.v` - inclusion of `{ x: X | P x }` into `X` is injective
- `Quotients.v` - quotients by equivalence relations, and induced functions on them
- `WellOrders.v` - some basic properties of well-orders, including a proof that Zorn's Lemma implies the well-ordering principle
- `ZornsLemma.v` - proof that choice implies Zorn's Lemma
---