Skip to content

Latest commit

 

History

History
191 lines (135 loc) · 7.06 KB

README.md

File metadata and controls

191 lines (135 loc) · 7.06 KB
Raw

Topology

Docker CI Contributing Code of Conduct Zulip

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):
  • License: GNU Lesser General Public License v2.1 or later
  • Compatible Coq versions: Coq 8.16 or later (use the corresponding branch or release for other Coq 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>

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