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)
  • stop-cran (@stop-cran)
  • Columbus240 (@Columbus240)
• License: GNU Lesser General Public License v2.1 or later
• Compatible Coq versions: Coq 8.16 / Rocq up to 9.2 (use the corresponding branch or release for other versions)
• Additional dependencies:
  • Zorn's Lemma (set library that is part of this repository)
• 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 both Topology and Zorn's Lemma manually, do:

git clone https://github.com/coq-community/topology.git
cd topology
make   # or make -j <number-of-cores-on-your-machine>

Working in the VS Code dev container

A ready-to-use development environment lives in .devcontainer/, based on ocaml/opam:debian-12-ocaml-4.14 (multi-arch: amd64 + arm64). The image pins Rocq 9.1 via opam and preinstalls dune, coq-lsp, and vsrocq-language-server so the VsRocq or coq-lsp VS Code clients work out of the box.

Open the repository in VS Code and run Dev Containers: Reopen in Container. The first build takes ~15-30 minutes (Rocq is compiled from source via opam); subsequent rebuilds reuse the Docker layer cache. Once inside, run make -j$(nproc) from the integrated terminal.

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

• FilterLimits.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
• AdjunctionSpace.v - quotient that glues a subspace to a point
• ContinuousFactorization.v - a continuous map factors through its image

Metric spaces

• MetricSpaces.v
• LipschitzMaps.v - Lipschitz-continuous maps between metric spaces
• Completeness.v
• Completion.v
• UniformTopology.v - the topology of uniform convergence
• BanachFixedPoint.v - the Banach fixed-point theorem for contractions on complete metric spaces

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

Worked examples

• Examples/S1.v - the unit circle as a quotient of [-1, 1]

Contents of Zorn's Lemma

In alphabetical order, except where related files are grouped together:

• Cardinals.v - collects the files in the folder Cardinals

• Cardinals/Cardinals.v defines cardinal comparisons for types

• Cardinals/CardinalsEns.v defines cardinal comparisons for ensembles

• Cardinals/Combinatorics.v defines some elementary bijections

• Cardinals/Comparability.v given choice, cardinals form a total order

• Cardinals/CSB.v prove Cantor-Schröder-Bernstein theorem

• Cardinals/Diagonalization.v Cantor's diagonalization and corollaries

• Cardinals/LeastCardinalsEns.v the cardinal orders are well-founded

• 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)

• DirectedSets.v - basics of directed sets

• Filters.v - basics of filters

• EnsembleProduct.v - products of ensembles, living in the type A * B

• EnsemblesImplicit.v - settings for appropriate implicit parameters for the standard library's Ensembles functions

• FiniteImplicit.v - same for the standard library's Sets/Finite_sets

• ImageImplicit.v - same for the standard library's Sets/Image

• Relation_Definitions_Implicit.v - same for the standard library's Relation_Definitions

• EnsemblesExplicit.v - clears the implicit parameters set in the above files

• 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.

• FunctionProperitesEns.v - same but definitions restricted to ensembles

• Image.v - images of subsets under functions

• InverseImage.v - inverse images of subsets under functions

• Ordinals.v - a construction of the ordinals without reference to well-orders

• 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

• ReverseMath - a folder with some results in constructive reverse mathematics

• 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

Bibliography

• Cunningham, D. W. (2016). "Set theory : a first course". Cambridge University Press. ISBN: 9781107120327
• Munkres, J. R. (2000). "Topology" (2nd ed.). Prentice-Hall. ISBN: 9780131816299
• Pradic, C. and Brown, C. E. (2019). "Cantor-Bernstein implies Excluded Middle". arXiv: https://arxiv.org/abs/1904.09193
• Preuss, G. (1975). "Allgemeine Topologie" (2., korr. Aufl.). Springer. ISBN: 3540074279