Skip to content

Commit f8a47c3

Browse files
Columbus240Columbus240
committed
Finite/Cardinals: Extract combinatorial lemmas
They hold independently of the def. `FiniteT` and are thus better placed in the Cardinals folder.
1 parent e3008c9 commit f8a47c3

File tree

4 files changed

+409
-360
lines changed

4 files changed

+409
-360
lines changed

‎_CoqProject

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ theories/Topology/Examples/S1.v
4040
theories/ZornsLemma/Cardinals.v
4141
theories/ZornsLemma/Cardinals/Cardinals.v
4242
theories/ZornsLemma/Cardinals/CardinalsEns.v
43+
theories/ZornsLemma/Cardinals/Combinatorics.v
4344
theories/ZornsLemma/Cardinals/Comparability.v
4445
theories/ZornsLemma/Cardinals/CSB.v
4546
theories/ZornsLemma/Cardinals/Diagonalization.v

‎theories/ZornsLemma/Cardinals.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
From ZornsLemma Require Export
33
Cardinals.Cardinals
44
Cardinals.CardinalsEns
5+
Cardinals.Combinatorics
56
Cardinals.CSB
67
Cardinals.Diagonalization
78
Cardinals.LeastCardinalsEns.

0 commit comments

Comments
 (0)