[B] Finite/Cardinals: Extract combinatorial lemmas

They hold independently of the def. `FiniteT` and are thus better placed in the Cardinals folder.
coq-community · Aug 18, 2024 · fbd613a · fbd613a
1 parent b99031b
commit fbd613a
Show file tree

Hide file tree

Showing 4 changed files with 409 additions and 360 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -40,6 +40,7 @@ theories/Topology/Examples/S1.v
 theories/ZornsLemma/Cardinals.v
 theories/ZornsLemma/Cardinals/Cardinals.v
 theories/ZornsLemma/Cardinals/CardinalsEns.v
+theories/ZornsLemma/Cardinals/Combinatorics.v
 theories/ZornsLemma/Cardinals/Comparability.v
 theories/ZornsLemma/Cardinals/CSB.v
 theories/ZornsLemma/Cardinals/Diagonalization.v

diff --git a/theories/ZornsLemma/Cardinals.v b/theories/ZornsLemma/Cardinals.v
@@ -2,6 +2,7 @@
 From ZornsLemma Require Export
   Cardinals.Cardinals
   Cardinals.CardinalsEns
+  Cardinals.Combinatorics
   Cardinals.CSB
   Cardinals.Diagonalization
   Cardinals.LeastCardinalsEns.