Formalize the Banach fixed-point theorem

One might want to move the more general lemmas to the coq stdlib or to `MetricSpaces.v`. For now this is fine.
coq-community · Oct 19, 2024 · 4b1f952 · 4b1f952
1 parent d5ddabf
commit 4b1f952
Show file tree

Hide file tree

Showing 2 changed files with 490 additions and 0 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -3,6 +3,7 @@
 -arg -set -arg "'Default Goal Selector=!'"
 
 theories/Topology/AdjunctionSpace.v
+theories/Topology/BanachFixedPoint.v
 theories/Topology/Compactness.v
 theories/Topology/Completeness.v
 theories/Topology/Completion.v