Skip to content

Commit 4427df1

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 c020d2d commit 4427df1

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
@@ -42,6 +42,7 @@ theories/Topology/Examples/S1.v
4242
theories/ZornsLemma/Cardinals.v
4343
theories/ZornsLemma/Cardinals/Cardinals.v
4444
theories/ZornsLemma/Cardinals/CardinalsEns.v
45+
theories/ZornsLemma/Cardinals/Combinatorics.v
4546
theories/ZornsLemma/Cardinals/Comparability.v
4647
theories/ZornsLemma/Cardinals/CSB.v
4748
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)