Finite/Cardinals: Extract combinatorial lemmas

They hold independently of the def. `FiniteT` and are thus better placed in the Cardinals folder.
coq-community · Oct 15, 2023 · 427ad66 · 427ad66
1 parent 6d48c2e
commit 427ad66
Show file tree

Hide file tree

Showing 4 changed files with 409 additions and 360 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -42,6 +42,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.