Restructure cardinals, finiteness and homeomorphisms

README.md

@@ -74,9 +74,7 @@ make   # or make -j <number-of-cores-on-your-machine>
 
 ### Filters and nets
 
-- `Filters.v`
 - `FilterLimits.v`
-- `DirectedSets.v`
 - `Nets.v`
 - `FiltersAndNets.v` - various transformations between filters and nets
 
@@ -123,8 +121,14 @@ topological spaces
 
 In alphabetical order, except where related files are grouped together:
 
-- `Cardinals.v` - cardinalities of sets
-- `Ordinals.v` - a construction of the ordinals without reference to well-orders
+- `Cardinals.v` - collects the files in the folder `Cardinals`
+- `Cardinals/Cardinals.v` defines cardinal comparisons for types
+- `Cardinals/CardinalsEns.v` defines cardinal comparisons for ensembles
+- `Cardinals/Combinatorics.v` defines some elementary bijections
+- `Cardinals/Comparability.v` given choice, cardinals form a total order
+- `Cardinals/CSB.v` prove Cantor-Schröder-Bernstein theorem
+- `Cardinals/Diagonalization.v` Cantor's diagonalization and corollaries
+- `Cardinals/LeastCardinalsEns.v` the cardinal orders are well-founded
 
 - `Classical_Wf.v` - proofs of the classical equivalence of wellfoundedness, the minimal element property, and the descending sequence property
 
@@ -134,9 +138,16 @@ In alphabetical order, except where related files are grouped together:
 
 - `DependentTypeChoice.v` - choice on a relation (`forall a: A, B a -> Prop`)
 
+- `DirectedSets.v` - basics of directed sets
+- `Filters.v` - basics of filters
+
+- `EnsembleProduct.v` - products of ensembles, living in the type `A * B`
+
 - `EnsemblesImplicit.v` - settings for appropriate implicit parameters for the standard library's Ensembles functions
+- `FiniteImplicit.v` - same for the standard library's Sets/Finite_sets
 - `ImageImplicit.v` - same for the standard library's Sets/Image
 - `Relation_Definitions_Implicit.v` - same for the standard library's Relation_Definitions
+- `EnsemblesExplicit.v` - clears the implicit parameters set in the above files
 
 - `EnsemblesSpec.v` - defines a notation for e.g. `[ n: nat | n > 5 /\ even n ] : Ensemble nat.`
 
@@ -154,9 +165,13 @@ In alphabetical order, except where related files are grouped together:
 - `InfiniteTypes.v` - same for infinite types
 
 - `FunctionProperties.v` - injective, surjective, etc.
+- `FunctionProperitesEns.v` - same but definitions restricted to ensembles
 
+- `Image.v` - images of subsets under functions
 - `InverseImage.v` - inverse images of subsets under functions
 
+- `Ordinals.v` - a construction of the ordinals without reference to well-orders
+
 - `Powerset_facts.v` - some lemmas about the operations on subsets that the stdlib is missing
 
 - `Proj1SigInjective.v` - inclusion of `{ x: X | P x }` into `X` is injective
@@ -168,3 +183,9 @@ In alphabetical order, except where related files are grouped together:
 - `WellOrders.v` - some basic properties of well-orders, including a proof that Zorn's Lemma implies the well-ordering principle
 
 - `ZornsLemma.v` - proof that choice implies Zorn's Lemma
+
+## Bibliography
+- Cunningham, D. W. (2016). "Set theory : a first course". Cambridge University Press. ISBN: 9781107120327
+- Munkres, J. R. (2000). "Topology" (2nd ed.). Prentice-Hall. ISBN: 9780131816299
+- Pradic, C. and Brown, C. E. (2019). "Cantor-Bernstein implies Excluded Middle". arXiv: https://arxiv.org/abs/1904.09193
+- Preuss, G. (1975). "Allgemeine Topologie" (2., korr. Aufl.). Springer. ISBN: 3540074279

_CoqProject

@@ -1,8 +1,6 @@
 -R theories/Topology Topology
 -R theories/ZornsLemma ZornsLemma
 -arg -set -arg "'Default Goal Selector=!'"
--arg -w -arg -deprecated-hint-rewrite-without-locality
--arg -w -arg -deprecated-instance-without-locality
 
 theories/Topology/AdjunctionSpace.v
 theories/Topology/Compactness.v
@@ -40,10 +38,15 @@ theories/Topology/UrysohnsLemma.v
 theories/Topology/WeakTopology.v
 theories/Topology/Examples/S1.v
 theories/ZornsLemma/Cardinals.v
-theories/ZornsLemma/CardinalsEns.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
+theories/ZornsLemma/Cardinals/LeastCardinalsEns.v
 theories/ZornsLemma/Classical_Wf.v
 theories/ZornsLemma/CountableTypes.v
-theories/ZornsLemma/CSB.v
 theories/ZornsLemma/DecidableDec.v
 theories/ZornsLemma/DependentTypeChoice.v
 theories/ZornsLemma/DirectedSets.v
@@ -64,7 +67,6 @@ theories/ZornsLemma/FunctionPropertiesEns.v
 theories/ZornsLemma/Image.v
 theories/ZornsLemma/ImageImplicit.v
 theories/ZornsLemma/IndexedFamilies.v
-theories/ZornsLemma/InfiniteTypes.v
 theories/ZornsLemma/InverseImage.v
 theories/ZornsLemma/Ordinals.v
 theories/ZornsLemma/Powerset_facts.v

meta.yml

@@ -99,9 +99,7 @@ documentation: |-
 
   ### Filters and nets
 
-  - `Filters.v`
   - `FilterLimits.v`
-  - `DirectedSets.v`
   - `Nets.v`
   - `FiltersAndNets.v` - various transformations between filters and nets
 
@@ -148,8 +146,14 @@ documentation: |-
 
   In alphabetical order, except where related files are grouped together:
 
-  - `Cardinals.v` - cardinalities of sets
-  - `Ordinals.v` - a construction of the ordinals without reference to well-orders
+  - `Cardinals.v` - collects the files in the folder `Cardinals`
+  - `Cardinals/Cardinals.v` defines cardinal comparisons for types
+  - `Cardinals/CardinalsEns.v` defines cardinal comparisons for ensembles
+  - `Cardinals/Combinatorics.v` defines some elementary bijections
+  - `Cardinals/Comparability.v` given choice, cardinals form a total order
+  - `Cardinals/CSB.v` prove Cantor-Schröder-Bernstein theorem
+  - `Cardinals/Diagonalization.v` Cantor's diagonalization and corollaries
+  - `Cardinals/LeastCardinalsEns.v` the cardinal orders are well-founded
 
   - `Classical_Wf.v` - proofs of the classical equivalence of wellfoundedness, the minimal element property, and the descending sequence property
 
@@ -159,9 +163,16 @@ documentation: |-
 
   - `DependentTypeChoice.v` - choice on a relation (`forall a: A, B a -> Prop`)
 
+  - `DirectedSets.v` - basics of directed sets
+  - `Filters.v` - basics of filters
+
+  - `EnsembleProduct.v` - products of ensembles, living in the type `A * B`
+
   - `EnsemblesImplicit.v` - settings for appropriate implicit parameters for the standard library's Ensembles functions
+  - `FiniteImplicit.v` - same for the standard library's Sets/Finite_sets
   - `ImageImplicit.v` - same for the standard library's Sets/Image
   - `Relation_Definitions_Implicit.v` - same for the standard library's Relation_Definitions
+  - `EnsemblesExplicit.v` - clears the implicit parameters set in the above files
 
   - `EnsemblesSpec.v` - defines a notation for e.g. `[ n: nat | n > 5 /\ even n ] : Ensemble nat.`
 
@@ -179,9 +190,13 @@ documentation: |-
   - `InfiniteTypes.v` - same for infinite types
 
   - `FunctionProperties.v` - injective, surjective, etc.
+  - `FunctionProperitesEns.v` - same but definitions restricted to ensembles
 
+  - `Image.v` - images of subsets under functions
   - `InverseImage.v` - inverse images of subsets under functions
 
+  - `Ordinals.v` - a construction of the ordinals without reference to well-orders
+
   - `Powerset_facts.v` - some lemmas about the operations on subsets that the stdlib is missing
 
   - `Proj1SigInjective.v` - inclusion of `{ x: X | P x }` into `X` is injective
@@ -193,4 +208,10 @@ documentation: |-
   - `WellOrders.v` - some basic properties of well-orders, including a proof that Zorn's Lemma implies the well-ordering principle
 
   - `ZornsLemma.v` - proof that choice implies Zorn's Lemma
+
+  ## Bibliography
+  - Cunningham, D. W. (2016). "Set theory : a first course". Cambridge University Press. ISBN: 9781107120327
+  - Munkres, J. R. (2000). "Topology" (2nd ed.). Prentice-Hall. ISBN: 9780131816299
+  - Pradic, C. and Brown, C. E. (2019). "Cantor-Bernstein implies Excluded Middle". arXiv: https://arxiv.org/abs/1904.09193
+  - Preuss, G. (1975). "Allgemeine Topologie" (2., korr. Aufl.). Springer. ISBN: 3540074279
 ---

theories/Topology/Compactness.v

@@ -616,27 +616,31 @@ Qed.
 Lemma topological_property_compact :
   topological_property compact.
 Proof.
-  intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hcomp F H eq.
+  apply Build_topological_property.
+  intros X Y f Hcont_f g Hcont_g Hfg Hcomp F H eq.
   destruct (Hcomp (inverse_image (inverse_image g) F)) as [F' [H1 [H2 H3]]].
   - intros.
-    rewrite <- (inverse_image_id_comp Hgf).
+    rewrite <- (inverse_image_id_comp (proj1 Hfg)).
     apply Hcont_f, H.
     now destruct H0.
   - erewrite <- inverse_image_full,
-             <- (inverse_image_id_comp Hgf (FamilyUnion _)).
+             <- (inverse_image_id_comp (proj1 Hfg) (FamilyUnion _)).
     f_equal.
-    now rewrite <- (inverse_image_family_union F Hgf),
-               inverse_image_id_comp.
+    erewrite <- inverse_image_family_union.
+    2, 3: apply Hfg.
+    rewrite inverse_image_id_comp; auto.
+    apply Hfg.
   - exists (inverse_image (inverse_image f) F').
     split; [|split].
     + apply injective_finite_inverse_image; auto.
       apply inverse_image_surjective_injective.
       apply invertible_impl_bijective.
-      exists g; assumption.
+      exists g; apply Hfg.
     + intros S [Hin].
       destruct (H2 _ Hin) as [H0].
-      now rewrite inverse_image_id_comp in H0.
-    + rewrite <- (inverse_image_family_union _ Hfg Hgf), H3.
+      rewrite inverse_image_id_comp in H0; auto.
+      apply Hfg.
+    + rewrite <- (inverse_image_family_union _ (proj2 Hfg) (proj1 Hfg)), H3.
       apply inverse_image_full.
 Qed.
 
@@ -683,8 +687,9 @@ Lemma compact_hausdorff_homeo {X Y : TopologicalSpace} (f : X -> Y) :
 Proof.
   intros.
   apply bijective_impl_invertible in H1.
-  destruct H1 as [g Hgf Hfg].
-  exists g; auto.
+  destruct H1 as [g [Hgf Hfg]].
+  split; auto.
+  exists g. repeat split; auto.
   apply continuous_closed.
   intros.
   assert (compact (SubspaceTopology U)) as HU_compact.

theories/Topology/Connectedness.v

@@ -117,18 +117,19 @@ Qed.
 Lemma topological_property_connected :
   topological_property connected.
 Proof.
-intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hconn S HS.
+apply Build_topological_property.
+intros X Y f Hf g Hg Hfg Hconn S HS.
 destruct (Hconn (inverse_image f S)) as [HfS|HfS];
 [ | left | right ];
   try extensionality_ensembles.
 - apply continuous_clopen; auto.
-- rewrite <- Hfg.
+- rewrite <- (proj2 Hfg).
   apply in_inverse_image.
   rewrite inverse_image_empty, <- HfS.
   constructor.
-  now rewrite Hfg.
+  now rewrite (proj2 Hfg).
 - constructor.
-- rewrite <- Hfg.
+- rewrite <- (proj2 Hfg).
   apply in_inverse_image.
   rewrite HfS.
   constructor.

theories/Topology/CountabilityAxioms.v

@@ -7,13 +7,12 @@ From Topology Require Export
   Nets
   SubspaceTopology.
 From ZornsLemma Require Export
-  CardinalsEns
+  Cardinals
   CountableTypes.
 From ZornsLemma Require Import
   Classical_Wf
   DecidableDec
-  FiniteIntersections
-  InfiniteTypes.
+  FiniteIntersections.
 From Coq Require Import
   RelationClasses.