meta.yml

---
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.16 or later (use the corresponding branch or release for other Coq versions)
  opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'

tested_coq_opam_versions:
- version: dev
- version: '8.19'
- version: '8.18'
- version: '8.17'
- version: '8.16'

dependencies:
- opam:
    name: dune
    version: '{>= "2.5"}'
- 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

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