Module docstring

Author: gasparattila

Mathlib/Topology/Sets/VietorisTopology.lean

@@ -11,7 +11,25 @@ public import Mathlib.Topology.Sets.Compacts
 # Vietoris topology
 
 This file defines the Vietoris topology on the types of compact subsets and nonempty compact subsets
-of a topological space.
+of a topological space. The Vietoris topology is generated by sets of the form
+$\{K \mid K \subseteq U\}$ and $\{K \mid K \cap U \ne \emptyset\}$, where $U$ is an open subset of
+the underlying space.
+
+## Implementation notes
+
+Rather than defining the topology directly on `TopologicalSpace.Compacts α`, we first define
+`TopologicalSpace.vietoris α` on `Set α`, then we take the subspace topology on
+`TopologicalSpace.Compacts α` and `TopologicalSpace.NonemptyCompacts α`. This approach will
+let us reuse several results if a type of closed sets equipped with the Vietoris topology is
+defined in the future.
+
+Note that we do not equip `TopologicalSpace.Closeds α` with the Vietoris topology. When `α` is a
+metric space, `TopologicalSpace.Closeds α` is equipped with the Hausdorff metric, which is generally
+incompatible with the Vietoris topology.
+
+## References
+
+* [Ernest Michael, *Topologies on spaces of subsets*][michael1951]
 -/
 
 @[expose] public section

docs/references.bib

@@ -3521,6 +3521,17 @@ @Book{            meyntweedie1993
   language      = {English}
 }
 
+@Article{         michael1951,
+  author        = {Michael, Ernest},
+  title         = {Topologies on spaces of subsets},
+  year          = {1951},
+  journal       = {Trans. Amer. Math. Soc.},
+  volume        = {71},
+  pages         = {152-182},
+  doi           = {10.1090/S0002-9947-1951-0042109-4},
+  url           = {https://doi.org/10.1090/S0002-9947-1951-0042109-4}
+}
+
 @Article{         Milla_2018,
   author        = {Milla, Lorenz},
   title         = {A detailed proof of the {C}hudnovsky formula with means of