complete changelog

CHANGELOG_UNRELEASED.md

@@ -28,21 +28,49 @@
   + lemmas `ereal_pseries_pred0`, `ub_ereal_sup_adherent_img`
   + definition `fsets`, lemmas `fsets_set0`, `fsets_self`, `fsetsP`, `fsets_img`
   + definition `fsets_ord`, lemmas `fsets_ord_nat`, `fsets_ord_subset`
-  + definition `gsum`, lemmas `gsum0`, `gsumE`, `gsum_ge0`, `gsum_fset`
-    `gsum_image`, `gsum_nat_lim`, `gsum_bigcup`
-  + notation `\gsum_(i in S) a i`
+  + definition `csum`, lemmas `csum0`, `csumE`, `csum_ge0`, `csum_fset`
+    `csum_image`, `ereal_pseries_csum`, `csum_bigcup`
+  + notation `\csum_(i in S) a i`
 - file `cardinality.v`
-  + defintion `surjective`
-  + definition `set_bijective`
+  + lemmas `in_inj_comp`, `enum0`, `enum_recr`, `eq_set0_nil`, `eq_set0_fset0`,
+    `image_nat_maximum`, `fset_nat_maximum`
+  + defintion `surjective`, lemmas `surjective_id`, `surjective_set0`,
+    `surjective_image`, `surjective_image_eq0`, `surjective_comp`
+  + definition `set_bijective`,
+  + lemmas `inj_of_bij`, `sur_of_bij`, `set_bijective1`, `set_bijective_image`,
+    `set_bijective_subset`, `set_bijective_comp`
   + definition `inverse`
+  + lemmas `inj_left_inverse`, `inj_right_inverse`, `sur_right_inverse`,
   + notation `` `I_n ``
-  + lemmas `pigeonhole`, `Cantor_Bernstein`
+  + lemmas `II0`, `II1`, `IIn_eq0`, `II_recr`
+  + lemmas `set_bijective_D1`, `pigeonhole`, `Cantor_Bernstein`
   + definition `card_le`, notation `_ #<= _`
+  + lemmas `card_le_surj`, `surj_card_le`, `card_lexx`, `card_le0x`,
+    `card_le_trans`, `card_le0P`, `card_le_II`
   + definition `card_eq`, notation `_ #= _`
+  + lemmas `card_eq_sym`, `card_eq_trans`, `card_eq00`, `card_eqP`, `card_eqTT`,
+    `card_eq_II`, `card_eq_le`, `card_eq_ge`, `card_leP`
+  + lemma `set_bijective_inverse`
   + definition `countable`
+  + lemmas `countable0`, `countable_injective`, `countable_trans`
   + definition `set_finite`
-  + definitions `enumeration`, `enum_wo_rep`
-  + lemmas `infinite_nat`, `infinite_prod_nat`
+  + lemmas `set_finiteP`, `set_finite_seq`, `set_finite_countable`, `set_finite0`
+  + lemma `set_finite_bijective`
+  + lemmas `subset_set_finite`, `subset_card_le`
+  + lemmas `injective_set_finite`, `injective_card_le`, `set_finite_preimage`
+  + lemmas `surjective_set_finite`, `surjective_card_le`
+  + lemmas `set_finite_diff`, `card_le_diff`
+  + lemmas `set_finite_inter_set0_union`, `set_finite_inter`
+  + lemmas `ex_in_D`, definitions `min_of_D`, `min_of_D_seq`, `infsub_enum`, lemmas
+    `min_of_D_seqE`, `increasing_infsub_enum`, `sorted_infsub_enum`,
+   `injective_infsub_enum`, `subset_infsub_enum`, `infinite_nat_subset_countable`
+  + definition `enumeration`, lemmas `enumeration_id`, `enumeration_set0`.
+  + lemma `ex_enum_notin`, definitions `min_of`, `minf_of_e_seq`, `smallest_of`
+  + definition `enum_wo_rep`, lemmas `enum_wo_repE`, `min_of_e_seqE`,
+    `smallest_of_e_notin_enum_wo_rep`, `injective_enum_wo_rep`, `surjective_enum_wo_rep`,
+    `set_bijective_enum_wo_rep`, `enumration_enum_wo_rep`, `countable_enumeration`
+  + lemmas `infinite_nat`, `infinite_prod_nat`, `countable_prod_nat`,
+    `countably_infinite_prod_nat`
 
 ### Changed
 

theories/cardinality.v

@@ -5,16 +5,16 @@ From mathcomp Require Import ssrnat seq fintype bigop div prime path finmap.
 Require Import boolp classical_sets.
 
 (******************************************************************************)
-(*                            Cardinality (WIP)                               *)
+(*                              Cardinality                                   *)
 (*                                                                            *)
 (* This file provides an account of cardinality properties of classical sets. *)
-(* This includes standard results such the Pigeon Hole principle or           *)
-(* Cantor-Bernstein Theorem.                                                  *)
+(* This includes standard results of naive set theory such as the Pigeon Hole *)
+(* principle or the Cantor-Bernstein Theorem.                                 *)
+(*                                                                            *)
 (* The contents of this file should not be considered as definitive because   *)
-(* it establishes too little connections with MathComp: finite sets are       *)
-(* defined using finmap's fsets but countability does not build on countType. *)
-(* Better interaction is explored in PR #83.                                  *)
-(* TODO: Look at fingroup/morphism.v for inspiration for better naming?       *)
+(* it establishes too little connections with MathComp: although finite sets  *)
+(* are defined using finmap's fsets but countability does not build on        *)
+(* countType. Improvement is explored in PR #83.                              *)
 (*                                                                            *)
 (*    surjective A B f == the function f whose domain is the set A and its    *)
 (*                        codomain is the set B is surjective                 *)
@@ -62,7 +62,7 @@ Import Order.TTheory.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-(* TODO: PR ?*)
+(* TODO: move *)
 Lemma in_inj_comp (A B C : Type) (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) :
   {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} ->
   {in Q &, injective (f \o h)}.
@@ -97,9 +97,10 @@ Qed.
 Lemma eq_set0_fset0 (T : choiceType) (S : {fset T}) :
   ([set x | x \in S] == set0) = (S == fset0).
 Proof. by rewrite eq_set0_nil. Qed.
+(* /TODO: move *)
 
 Lemma image_nat_maximum n (f : nat -> nat) :
-  (exists i, i <= n /\ (forall j, j <= n -> f j <= f i))%N.
+  (exists i, i <= n /\ forall j, j <= n -> f j <= f i)%N.
 Proof.
 elim: n => [|n [j [jn1 nfj]]]; first by exists 0%N; split => //; case.
 have [fn1fj|fjfn1] := leP (f n.+1) (f j).
@@ -124,7 +125,6 @@ have [k [kA <-]] : exists k, (k < #|` A|)%N /\ f k = j.
 rewrite H //.
 by move: kA; rewrite -(@prednK #|` A|) // cardfs_gt0.
 Qed.
-(* End: TODO: PR ?*)
 
 Definition surjective aT rT (A : set aT) (B : set rT) (f : aT -> rT) :=
   forall u, B u -> exists t, A t /\ u = f t.
@@ -175,7 +175,7 @@ Proof. by case. Qed.
 Lemma sur_of_bij A B f : set_bijective A B f -> surjective A B f.
 Proof. by case. Qed.
 
-Lemma set_bijectiveE A B f g : {in A, f =1 g} ->
+Lemma set_bijective1 A B f g : {in A, f =1 g} ->
   set_bijective A B f -> set_bijective A B g.
 Proof.
 move=> fg bij_f; split.
@@ -186,11 +186,11 @@ move=> fg bij_f; split.
   by exists t; split => //; rewrite -fg// in_setE.
 Qed.
 
-Lemma injective_set_bijective A f :
+Lemma set_bijective_image A f :
   {in A &, injective f} -> set_bijective A (f @` A) f.
 Proof. by move=> fi; split => // u [t At <-{u}]; exists t. Qed.
 
-Lemma set_bijective_sub A B f :
+Lemma set_bijective_subset A B f :
   set_bijective A B f -> forall B0, B0 `<=` B ->
   set_bijective ((f @^-1` B0) `&` A) B0 f.
 Proof.
@@ -485,7 +485,7 @@ Lemma card_leP (T U : pointedType) (A : set T) (B : set U) :
 Proof.
 split=> [[f [fi fAB]]|[C [CB /card_eq_sym AC]]]; last first.
  by apply: (card_eq_ge AC); exists id; split => //; rewrite image_id.
-have AfAf := injective_set_bijective fi.
+have AfAf := set_bijective_image fi.
 by exists (f @` A); split => //; apply/card_eqP; exists f.
 Qed.
 
@@ -554,7 +554,7 @@ Proof. by exists fset0; rewrite predeqE. Qed.
 
 Section set_finite_bijection.
 
-Lemma set_bijective_U1 (T : pointedType) n (f g : nat -> T) (A : set T) :
+Local Lemma set_bijective_U1 (T : pointedType) n (f g : nat -> T) (A : set T) :
   set_bijective `I_n.+1 A f ->
   set_bijective `I_n (A `\ f n) g ->
   set_bijective `I_n.+1 A (fun m => if (m < n)%N then g m
@@ -592,7 +592,7 @@ move=> bij_f bij_g; split.
   by exists j; split; [rewrite (ltn_trans jn) | rewrite jn -tgj].
 Qed.
 
-Lemma set_bijective_cyclic_shift (T : pointedType) n (f g : nat -> T) (A : set T) :
+Local Lemma set_bijective_cyclic_shift (T : pointedType) n (f g : nat -> T) (A : set T) :
   set_bijective `I_n.+1 A f ->
   set_bijective `I_n (A `\ f n) g ->
   set_bijective `I_n.+1 A (fun m => if m == 0%N then f n
@@ -634,13 +634,14 @@ move=> bij_f bij_g; split.
   by exists j.+1; split; [rewrite ltnS|rewrite /= ltnS jn tfi].
 Qed.
 
-Lemma set_bijective_cyclic_shift_simple (T : pointedType) n (f : nat -> T) (A : set T) :
+Local Lemma set_bijective_cyclic_shift_simple (T : pointedType) n (f : nat -> T)
+    (A : set T) :
   set_bijective `I_n.+1 A f ->
   set_bijective `I_n.+1 A (fun m => if m is 0%N then f n else f m.-1).
 Proof.
 move=> bij_f.
 have := set_bijective_cyclic_shift bij_f (set_bijective_D1 bij_f).
-apply: set_bijectiveE => i; rewrite in_setE => ni1.
+apply: set_bijective1 => i; rewrite in_setE => ni1.
 by case: ifPn => [/eqP -> //|i0]; rewrite ni1; case: i ni1 i0.
 Qed.
 
@@ -652,8 +653,7 @@ Proof.
 case: n S => [S /set0P A0 Ac0 _|n S].
   suff : A #= @set0 T by move/card_eq0/eqP; rewrite (negbTE A0).
   move/card_eq_trans : Ac0; apply.
-  rewrite (_ : (fun n : nat => _) = set0); last by rewrite predeqE => -[].
-  exact: card_eq00.
+  by rewrite II0; exact: card_eq00.
 move: n A S; elim=> [A S [t At] A1 SA|n ih A S A0 /card_eq_sym].
   have {}At : A = [set t].
     rewrite predeqE => t'; split=> [At'|->//].
@@ -768,7 +768,7 @@ have [/eqP B0|/set0P B0] := boolP (B == set0).
   move: AB; rewrite B0 subset0 => ->.
   by split; [exact: set_finite0|exact: card_le0x].
 have [f [bij_f [k [kn fAk]]]] := set_finite_bijective B0 Bn AB.
-have := set_bijective_sub bij_f AB.
+have := set_bijective_subset bij_f AB.
 rewrite fAk => bij_f1; split.
   by apply/set_finiteP; exists k; exact/card_eqP/set_bijective_inverse/bij_f1.
 apply: (@card_eq_le _ _ _ `I_n); first exact: card_eq_sym.
@@ -796,7 +796,7 @@ have [B0|/set0P/negP/negPn/eqP B0] := pselect (B !=set0); last first.
 case: (@set_finite_bijective U B n (f @` A) B0 Bn fAB) => h [bij_h [k [kn gfA]]].
 have finfA : set_finite (f @` A).
   by apply: (subset_set_finite fAB _); apply/set_finiteP; exists n.
-have AfAf := injective_set_bijective inj_f.
+have AfAf := set_bijective_image inj_f.
 have finA : set_finite A.
   move/set_finiteP in finfA.
   case: finfA => m /card_eq_sym mfA; apply/set_finiteP; exists m.
@@ -866,9 +866,18 @@ Lemma surjective_card_le
   surjective A B f -> set_finite A -> B #<= A.
 Proof. by move=> ABf fA; have [] := surjective_set_finite_card_le ABf fA. Qed.
 
-Corollary set_finite_diff (T : pointedType) (A B : set T) : set_finite A ->
-  set_finite (A `\` B) /\ A `\` B #<= A.
-Proof. by apply: subset_set_finite_card_le => t []. Qed.
+Lemma set_finite_diff (T : pointedType) (A B : set T) : set_finite A ->
+  set_finite (A `\` B).
+Proof.
+move=> fA.
+by have [] := (@subset_set_finite_card_le _ (A `\` B) A) _ fA => // t [].
+Qed.
+
+Lemma card_le_diff (T : pointedType) (A B : set T) : set_finite A ->
+  A `\` B #<= A.
+move=> fA.
+by have [] := (@subset_set_finite_card_le _ (A `\` B) A) _ fA => // t [].
+Qed.
 
 Lemma set_finite_inter_set0_union (T : pointedType) (A B : set T) :
   set_finite A -> set_finite B -> A `&` B = set0 -> set_finite (A `|` B).