WIP: Sketch some theory about euclidean spaces

Highlights: - FiniteProducts (i.e. spaces of the form X^n) - The skeleton of a vector structure on ℝ^n - The Heine-Borel property - Define spheres and show that spheres are compact
coq-community · Jun 2, 2021 · 850ee2e · 850ee2e
1 parent 0d14ee2
commit 850ee2e
Show file tree

Hide file tree

Showing 2 changed files with 522 additions and 0 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -8,6 +8,7 @@ theories/Topology/Connectedness.v
 theories/Topology/Continuity.v
 theories/Topology/ContinuousFactorization.v
 theories/Topology/CountabilityAxioms.v
+theories/Topology/EuclideanSpaces.v
 theories/Topology/FilterLimits.v
 theories/Topology/FiltersAndNets.v
 theories/Topology/Homeomorphisms.v