Topology
This library develops some of the basic concepts and results of general topology in Coq.
Meta
-
Author(s):
- Daniel Schepler (initial)
-
Coq-community maintainer(s):
- Andrew Miloradovsky (@amiloradovsky)
-
Compatible Coq versions: Coq 8.11 or later (use the corresponding branch or release for other Coq versions)
-
Additional dependencies:
-
Coq namespace:
Topology
-
Related publication(s): none
Building and installation instructions
The easiest way to install the latest released version of Topology is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-topology
To instead build and install manually, do:
git clone https://github.com/coq-community/topology.git
cd topology
make # or make -j <number-of-cores-on-your-machine>
make install
Contents, 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, LindelofSeparatednessAxioms.v
- T0, T1, Hausdorff, etc.
General constructions of topologies
OrderTopology.v
StrongTopology.v
- strong topology induced by a family of maps from topological spacesWeakTopology.v
- weak topology induced by a family of maps to topological spacesProductTopology.v
SubspaceTopology.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 RRFuncContinuity.v
- reproof of continuity of basic functions on R
"First nontrivial results of topology"
UrysohnsLemma.v
TietzeExtension.v