Library set10

Theory of Sets EIII-6 Infinite sets

Copyright INRIA (2009) Apics Team (Jose Grimm).

Require Export set2.
Require Export set3.
Require Export set4.
Require Export set5.
Require Export set6.
Require Export set7.
Require Export set9.

Set Implicit Arguments.

Module InfiniteSets.

EIII-6-1 The set of natural integers


Lemma equipotent_nat_Bnat: equipotent Bnat nat.
Proof. exists (BL (fun z => Ro (cardinal_nat z)) Bnat nat). aw. eee.
  app bl_bijective.
  red. ir. app R_inc.
  ir. wr (nat_to_B_pr H). wr (nat_to_B_pr H0). rww (R_inj H1).
  ir. nin H. exists (nat_to_B x). split. fprops. aw.
Qed.

Lemma infinite_Bnat: is_infinite_c (cardinal Bnat).
Proof. ir. assert (cardinal Bnat = cardinal nat). aw.
  ap equipotent_nat_Bnat. rw H. app nat_infinite_set.
Qed.

EIII-6-2 Definition of mappings by induction


Lemma segment_Bnat_order: forall x, inc x Bnat ->
  segment Bnat_order x = interval_co Bnat_order card_zero x.
Proof. ir. uf segment. uf_interval. uf glt.
  set_extens; Ztac; eee. rw Bnat_order_le. rwi Bnat_order_le H2. red in H2.
  red. eee.
Qed.

Definition induction_defined s a:= choose(fun f=>
  source f = Bnat & surjective f & W card_zero f = a &
  forall n, inc n Bnat -> W (succ n) f = s (W n f)).

Definition induction_defined0 h a := choose(fun f=>
  source f = Bnat & surjective f & W card_zero f = a &
  forall n, inc n Bnat -> W (succ n) f = h n (W n f)).

Definition induction_defined1 h a p := choose(fun f=>
  source f = Bnat & surjective f & W card_zero f = a &
  (forall n, cardinal_lt n p -> W (succ n) f = h n (W n f)) &
  (forall n, inc n Bnat -> ~ (cardinal_le n p) -> W n f = a)).

Definition induction_defined_set s a E:= choose(fun f=>
  is_function f &source f = Bnat & target f = E & W card_zero f = a &
  forall n, inc n Bnat -> W (succ n) f = s (W n f)).

Definition induction_defined0_set h a E:= choose(fun f=>
  is_function f & source f = Bnat & target f = E & W card_zero f = a &
  forall n, inc n Bnat -> W (succ n) f = h n (W n f)).

Definition induction_defined1_set h a p E := choose(fun f=>
  is_function f &source f = Bnat & target f = E & W card_zero f = a &
  (forall n, cardinal_lt n p -> W (succ n) f = h n (W n f)) &
  (forall n, inc n Bnat -> ~ (cardinal_le n p) -> W n f = a)).

Lemma integer_induction0: forall h a,
  exists_unique (fun f=> source f = Bnat & surjective f &
    W card_zero f = a
    & forall n, inc n Bnat -> W (succ n) f = h n (W n f)).
Proof. ir. split. set (M := fun u => cardinal (source u)).
  set (p:= fun u => Yo(M u = card_zero) a (h (predc (M u))(W (predc (M u)) u))).
  cp Bnat_order_worder. nin (transfinite_definition p H). clear H1.
  nin H0. ufi transfinite_def H0. rwi Bnat_order_substrate H0. ee.
  ufi restriction_to_segment H2. ufi p H2.
  assert(forall a, inc a Bnat -> M (restriction1 x (segment Bnat_order a))
    = a). ir. uf restriction1. uf M. aw. rww segment_Bnat_order.
  rww cardinal_interval_co_0a1.
  exists x. ee. am. am. rw (H2 _ inc0_Bnat). rw (H3 _ inc0_Bnat). rww Y_if_rw.
  ir. assert (inc (succ n) Bnat). fprops. rw (H2 _ H5). rw (H3 _ H5).
  rw Y_if_not_rw. rw predc_pr1.
  rww restriction1_W. fct_tac. rw H1. rww segment_Bnat_order.
  app sub_interval_co_0a_Bnat. rww segment_Bnat_order.
  rww interval_co_0a_pr3. fprops. fprops. app succ_nonzero.
  ir. ee. app function_exten4. ue. rw H.
  app cardinal_c_induction_v. ue. ir. rw H6. rw H3. ue. am. am.
Qed.

Lemma integer_induction: forall s a, exists_unique (fun f =>
  source f = Bnat & surjective f & W card_zero f = a &
  forall n, inc n Bnat -> W (succ n) f = s (W n f)).
Proof. ir. set (h:= fun _ x:Set => s x).
  nin (integer_induction0 h a). split. nin H. exists x. auto.
  ir. app H0.
Qed.

Lemma integer_induction1: forall h a p, inc p Bnat ->
  exists_unique (fun f=> source f = Bnat & surjective f &
    W card_zero f = a &
     (forall n, cardinal_lt n p -> W (succ n) f = h n (W n f))&
     (forall n, inc n Bnat -> ~ (cardinal_le n p) -> W n f = a)).
Proof. ir. split. set (h1:= fun n x => Yo (cardinal_lt n p) (h n x) a).
  nin (integer_induction0 h1 a). clear H1. nin H0. exists x. ee.
  am. am. ue. ir. rw H3. uf h1. rww Y_if_rw. nin H4. Bnat_tac.
  ir. assert (n <> card_zero). dneg. rw H6. fprops.
  bwi H4. cp (predc_pr H4 H6). ee. rw H8. rw H3. uf h1.
  rww Y_if_not_rw. wr lt_n_succ_le. ue. bw. am. bw.
  ir. ee. app function_exten4. ue. rw H0. app cardinal_c_induction_v.
  ue. ir. nin (p_or_not_p (cardinal_lt n p)). ir. rww H8. rww H4. ue.
  ir. assert (~ cardinal_le (succ n) p). srw. fprops. fprops.
  rww H9. rww H5. fprops. fprops.
Qed.

Lemma induction_defined_pr: forall s a,
  let f := induction_defined s a in
     source f = Bnat & surjective f & W card_zero f = a &
     forall n, inc n Bnat -> W (succ n) f = s (W n f).
Proof. ir. uf f. uf induction_defined. app choose_pr.
  nin (integer_induction s a). am.
Qed.

Lemma induction_defined_pr0: forall h a,
  let f := induction_defined0 h a in
     source f = Bnat & surjective f & W card_zero f = a &
     forall n, inc n Bnat -> W (succ n) f = h n (W n f).
Proof. ir. uf f. uf induction_defined0. app choose_pr.
  nin (integer_induction0 h a). am.
Qed.

Lemma induction_defined_pr1: forall h a p,
  let f := induction_defined1 h a p in
    inc p Bnat ->
    ( source f = Bnat & surjective f &
      W card_zero f = a &
      (forall n, cardinal_lt n p -> W (succ n) f = h n (W n f))&
      (forall n, inc n Bnat -> ~ (cardinal_le n p) -> W n f = a)).
Proof. ir. uf f. uf induction_defined1. app choose_pr.
  nin (integer_induction1 h a H). am.
Qed.

Lemma integer_induction_stable: forall E g a,
  inc a E -> (forall x, inc x E -> inc (g x) E) ->
  sub (target (induction_defined g a)) E.
Proof. ir. cp (induction_defined_pr g a).
  set (f:= induction_defined g a) in *. simpl in H1. ee. red.
  assert (forall n, inc n Bnat -> inc (W n f) E). app cardinal_c_induction_v.
  ue. ir. rww H4. app H0.
  ir. nin (surjective_pr2 H2 H6). nin H7. wr H8. app H5. ue.
Qed.

Lemma integer_induction_stable0: forall E h a,
  inc a E -> (forall n x, inc x E -> inc n Bnat -> inc (h n x) E) ->
  sub (target (induction_defined0 h a)) E.
Proof. ir. cp (induction_defined_pr0 h a).
  set (f:= induction_defined0 h a) in *. simpl in H1. ee. red.
  assert (forall n, inc n Bnat -> inc (W n f) E). app cardinal_c_induction_v.
  rww H3. ir. rww H4. app H0. ir.
  nin (surjective_pr2 H2 H6). nin H7. wr H8. app H5. ue.
Qed.

Lemma integer_induction_stable1: forall E h a p,
  inc p Bnat ->
  inc a E -> (forall n x, inc x E -> cardinal_lt n p -> inc (h n x) E) ->
  sub (target (induction_defined1 h a p)) E.
Proof. ir. cp (induction_defined_pr1 h a H).
  set (f:= induction_defined1 h a p) in *. simpl in H1. ee. red.
  assert (forall n, inc n Bnat -> inc (W n f) E). app cardinal_c_induction_v.
  rww H4. ir. nin (p_or_not_p (cardinal_lt n p)). ir. rww H5. app H1.
  ir. assert (~ cardinal_le (succ n) p). srw. fprops. fprops. rww H6.
  fprops.
  ir. nin (surjective_pr2 H3 H8). nin H9. wr H10. app H7. ue.
Qed.

Lemma induction_defined_pr_set: forall E g a,
  let f := induction_defined_set g a E in
    inc a E -> (forall x, inc x E -> inc (g x) E) ->
     (is_function f & source f = Bnat & target f = E & W card_zero f = a &
     forall n, inc n Bnat -> W (succ n) f = g (W n f)).
Proof. ir. uf f. uf induction_defined_set. app choose_pr. clear f.
  cp (induction_defined_pr g a).
  cp (integer_induction_stable H H0). simpl in H1. ee.
  set (h:= induction_defined g a) in *.
  set (f:= corresp Bnat E (graph h)).
  assert (is_function f). uf f. nin H3. nin H3. ee. app is_function_pr.
  fprops. apply sub_trans with (target h). fprops. am. ue.
  exists f. ee. am. uf f. aw. uf f. aw. uf f. uf W. aw. uf f. uf W. aw.
Qed.

Lemma induction_defined_pr_set0: forall E h a,
  let f := induction_defined0_set h a E in
    inc a E -> (forall n x, inc x E -> inc n Bnat -> inc (h n x) E) ->
     (is_function f & source f = Bnat & target f = E & W card_zero f = a &
     forall n, inc n Bnat -> W (succ n) f = h n (W n f)).
Proof. ir. uf f. uf induction_defined0_set. app choose_pr. clear f.
  cp (induction_defined_pr0 h a).
  cp (integer_induction_stable0 H H0). simpl in H1. ee.
  set (h0:= induction_defined0 h a) in *.
  set (f:= corresp Bnat E (graph h0)).
  assert (is_function f). nin H3. nin H3. ee. uf f. app is_function_pr.
  apply sub_trans with (target h0). fprops. am. ue.
  exists f. ee. am. uf f. aw. uf f. aw. uf f; uf W; aw. uf f. uf W. aw.
Qed.

Lemma induction_defined_pr_set1: forall E h a p,
  let f := induction_defined1_set h a p E in
    inc p Bnat ->
    inc a E -> (forall n x, inc x E -> cardinal_lt n p -> inc (h n x) E) ->
    (is_function f & source f = Bnat & target f = E & W card_zero f = a &
      (forall n, cardinal_lt n p -> W (succ n) f = h n (W n f))&
      (forall n, inc n Bnat -> ~ (cardinal_le n p) -> W n f = a)).
Proof. ir. uf f. uf induction_defined1_set. app choose_pr. clear f.
  cp (induction_defined_pr1 h a H).
  cp (integer_induction_stable1 H H0 H1). simpl in H2. ee.
  set (h0:= induction_defined1 h a p) in *.
  set (f:= corresp Bnat E (graph h0)). assert (is_function f).
  nin H4. nin H4. ee. uf f. app is_function_pr.
  apply sub_trans with (target h0). fprops. am. ue.
  exists f. ee. am. uf f. aw. uf f. aw. uf f; uf W; aw. uf f. uf W. aw.
  uf f. uf W. aw.
Qed.

EIII-6-3 Properties of infinite cardinals

Lemma equipotent_range: forall f, injective f ->
  equipotent (source f) (range (graph f)).
Proof. ir. set (ci:= canonical_injection (range (graph f)) (target f)).
  set (g0:= restriction2 f (source f) (range (graph f))).
  assert (is_function f). fct_tac.
  cp (canonical_decomposition1 H0 (refl_equal g0) (refl_equal ci)).
  ee. pose (H5 H). exists g0. ee; tv; uf g0; uf restriction2; aw.
Qed.

Lemma morphism_range: forall f a b,
  order_morphism f a b -> equipotent (substrate a) (range (graph f)).
Proof. ir. red in H. ee. rw H2. app equipotent_range.
Qed.

Lemma morphism_range1: forall f a b,
  order_morphism f a b -> cardinal (substrate a) = cardinal (range (graph f)).
Proof. ir. aw. app (morphism_range H).
Qed.

Lemma infinite_greater_countable: forall E,
  infinite_set E -> exists F, sub F E & cardinal F = cardinal Bnat.
Proof. ir. nin (Zermelo E). cp Bnat_order_worder. nin H0.
  nin (isomorphism_worder H0 H1). nin H3. clear H4. nin H3. nin H3.
  cp (morphism_range1 H4). rwi H2 H5.
  nin (well_ordered_segment H1 H3). rwi Bnat_order_substrate H6.
  exists E. split. fprops. ue.
  nin H6. nin H6. rwi Bnat_order_substrate H6. rwi (segment_Bnat_order H6) H7.
  cp (finite_set_interval_co H6). wri H7 H8. nin H. elim H9. rw H5. exact H8.
  nin H3. clear H4. nin H3. ee. cp (morphism_range1 H4).
  rwi Bnat_order_substrate H5. rw H5. exists (range (graph x0)).
  split. red in H3. ee. ue. tv.
Qed.

Lemma equipotent_N2_N: equipotent (product Bnat Bnat) Bnat.
Proof. set (mi:= fun n m => n + binom (n+m+1) 2).
  assert (Ha: forall n m, binom (n+m+1) 2 <= mi n m). ir. uf mi. app le_plus_r.
  assert (Hb:forall n m, mi n m < binom (S (n+m+1)) 2).
  ir. simpl. uf mi. set (t:= binom (n + m + 1) 2). rw plus_comm. rw binom1.
  app plus_lt_compat_l. wr plus_assoc. app lt_plus. rw plus_comm. simpl. autoa.
  exists (BL (fun z => nat_to_B(mi (cardinal_nat (P z))
    (cardinal_nat (Q z)))) (product Bnat Bnat) Bnat). ee; aw; tv.
  app bl_bijective. red. ir. fprops. ir. cp (nat_B_inj _ _ H1).
  set (a:= cardinal_nat (P u)) in *. set (b:= cardinal_nat (Q u)) in *.
  set (c:= cardinal_nat (P v)) in *. set (d:= cardinal_nat (Q v)) in *.
  cp (Ha a b). cp (Ha c d). cp (Hb a b). cp (Hb c d). rwi H2 H5; rwi H2 H3.
  cp (le_lt_trans _ _ _ H3 H6). cp (le_lt_trans _ _ _ H4 H5).
  assert (Ht:forall n m, binom (n+1) 2 < binom (S (m+1)) 2 -> n<=m).
  ir. assert (n +1 < S (m +1)). rww (binom_monotone2 (k:=2)). au. autoa. autoa.
  red in H10. app (plus_le_reg_l n m 1). rw plus_comm; rw (plus_comm 1 m).
  autoa. cp (Ht _ _ H7). cp (Ht _ _ H8). cp (le_antisym _ _ H9 H10).
  ufi mi H2. rwi H11 H2. cp (plus_reg_r _ _ _ H2).
  rwi H12 H11. cp (plus_reg_l _ _ _ H11). awi H. awi H0. ee.
  app pair_extensionality. wr (nat_to_B_pr H14). wr (nat_to_B_pr H16).
  fold a. fold c. ue. wr (nat_to_B_pr H17). wr (nat_to_B_pr H15).
  fold b. fold d. ue.
  assert (forall y, 0<> y -> exists n, exists m, mi n m = y). ir.
  set (p:= fun k=> y < binom (S k) 2). assert (~ p 0). uf p. simpl. autoa.
  assert (exists n, p n). uf p. exists (S y). simpl.
  rw binom1. rw binom0. wr plus_assoc. rw plus_comm. wr plus_assoc.
  app lt_plus. rw (plus_comm y 1). wr plus_assoc. wr Sn_is_1plus. auto.
  nin (least_int_prop0 _ H0 H1). ufi p H2. nin H2.
  set (A:= binom (S x) 2) in *.
  assert (binom (S (S x)) 2 = A + S x). uf A. simpl. rw binom1.
  rw binom0. rw (Sn_is_1plus x). rww (plus_comm 1 x). rwi H4 H2. clear H4.
  assert (y <= A+x). app le_S_n. assert (S (A + x) = A + S x). autoa. ue.
  nin (le_or_lt A y). cp (le_plus_minus _ _ H5). rwi plus_comm H6.
  set (m:= x - (y-A)).
  assert (S x = (y-A) + m +1). rw plus_comm. rw Sn_is_1plus.
  cut (x = y - A + m). ir. ue. uf m. sy. app le_plus_minus_r.
  app (plus_le_reg_l (y - A) x A). rw plus_comm. ue.
  exists (y-A). exists m. uf mi. wrr H7. au. contradiction.
  ir. set (x:= cardinal_nat y).
  assert (exists n, exists m, mi n m = x). case x. exists 0; exists 0. tv.
  ir. app H. nin H1; nin H1.
  exists (J (nat_to_B x0) (nat_to_B x1)). split. fprops. aw. rw H1. uf x. aw.
Qed.

Theorem equipotent_inf2_inf: forall a, is_infinite_c a ->
  card_pow a (card_two) = a.
Proof. ir. rename a into E. rename H into Hi.
  assert (Ha:is_cardinal E). red in Hi. ee. am.
  assert (Hb:cardinal E = E). fprops.
  assert (Hj:infinite_set E). red. rw Hb. am.
  set (base := set_of_sub_functions E (product E E)).
  set (pr := fun z => injective z & range (graph z) = coarse (source z)).

  assert (exists psi, inc psi base & pr psi & infinite_set (source psi)).
  nin (infinite_greater_countable Hj). ee. assert (equipotent x (product x x)).
  awi H0. eqsym. eqtrans (product Bnat Bnat). app equipotent_product.
  eqtrans Bnat. ap equipotent_N2_N. eqsym. am. nin H1. ee.
  assert (transf_axioms (fun z => W z x0) x (product E E)). red. ir.
  assert (sub (product x x) (product E E)). app product_monotone. app H5.
  wr H3. app inc_W_target. fct_tac. ue.
  set (y:= BL (fun z => W z x0) x (product E E)). assert (injective y).
  uf y. app bl_injective. ir. nin H1. nin H1. app H9. ue. ue. exists y. ee.
  uf base. Ztac. bw. split. fct_tac. uf y. aw. au. uf pr. ee. am. uf y. aw.
  uf BL. rw corresp_graph. uf coarse. wr H3. set_extens. rwi L_range_rw H6.
  nin H6. ee. wr H7. app inc_W_target. fct_tac. ue. rw L_range_rw. nin H1.
  nin (surjective_pr2 H7 H6). wr H2. nin H8. ex_tac. uf y. aw. red.
  rw H0. app infinite_Bnat. nin H. rename x into psi.
  destruct H as [ Hpsibase [ Hprpsi Hsrcpsi ]].
  set (odr := opposite_order (extension_order E (product E E))).
  set (ind := Zo base (fun z => pr z & sub (graph psi) (graph z))).
  assert (Hy:order (extension_order E (product E E))). fprops.
  assert (Hx:order odr). uf odr. fprops.
  assert (Hz:sub ind (substrate odr)). uf odr. aw. fold base. uf ind. app Z_sub.
  assert (Hw:order (induced_order odr ind)). fprops.
  assert (Hind : inductive_set (induced_order odr ind)).
  cp (extension_is_order E (product E E)). red. ir. red in H1. awii H1. awii H0.
  assert (Hla:forall i, inc i X -> is_function i).
  ir. cp (H0 _ H2). ufi ind H3. Ztac. ufi pr H5. ee. fct_tac.
  assert (Hlb:forall i, inc i X -> target i = product E E).
  ir. cp (H0 _ H2). ufi ind H3. Ztac. ufi base H4. bwi H4. ee. am.
  assert (Hlc: forall x y, inc x X -> inc y X -> gle odr x y \/ gle odr y x).
  ir. nin H1. set (H4 _ _ H2 H3). ufi gge H3. nin o;
  cp (related_induced_order1 H5); cp (related_induced_order1 H6); au.
  assert (Hd: forall i j, inc i X -> inc j X ->
   agrees_on (intersection2 (source i) (source j)) i j).
  ir. red. ee. app intersection2sub_first. app intersection2sub_second. ir.
  nin (intersection2_both H5). nin (Hlc _ _ H2 H3); [ | sy ];
  app (extension_order_pr H8 (x:=a)).
  assert (He:forall i, inc i X -> function_prop i (source i) (product E E)).
  ir. red. ee. app Hla. tv. app Hlb.
  nin H1. cp (extension_covering _ _ He Hd). nin H3. clear H4. nin H3. ee.
  red in H3. ee. assert (inc x base). uf base. bw. eee. red. ir.
  nin (unionf_exists H7). nin H8. cp (H0 _ H8). ufi ind H10. Ztac.
  ufi base H11. bwi H11. ee. app H14.
  assert (Hf: forall i, inc i X -> agrees_on (source i) i x).
  ir. cp (H4 _ H8). red in H9. red. ee. am. am. ir. sy. app H11.
  assert (Hg: forall i, inc i X -> sub (graph i) (graph x)). ir.
  cp (Hf _ H8). rww sub_function. app Hla.
  nin (emptyset_dichot X). exists psi. red. split. aw. uf ind. Ztac. fprops.
  rw H8. ir. elim (emptyset_pr H9). nin H8.
  assert(sub (graph psi) (graph x)). apply sub_trans with (graph y).
  assert (inc y ind). app H0. ufi ind H9. Ztac. ee. am. app Hg.
  assert (injective x). red. split. am. ir.
  rwi H5 H10. rwi H5 H11. nin (unionf_exists H10). nin (unionf_exists H11). ee.
  assert (exists z, inc z X & inc x0 (source z) & inc y0 (source z)).
  cp (Hlc _ _ H13 H14). ufi odr H17. awii H17.
  nin H17; ee; cp (source_extends H19); [exists x2 | exists x1 ]; eee.
  nin H17. ee. cp (H0 _ H17). ufi ind H20. Ztac. ufi pr H22. ee. nin H22.
  app H25. cp (H4 _ H17). red in H26. ee. wrr H28. wrr H28.
  assert (range (graph x) = product (source x) (source x)).
  set_extens. awi H11. nin H11. cp (inc_pr1graph_source H3 H11).
  rwi H5 H12. rwi unionf_rw H12. nin H12. nin H12.
  cp (W_pr H3 H11). cp (H4 _ H12). red in H15. ee. rwi (H17 _ H13) H14.
  cp (H0 _ H12). ufi ind H18. Ztac. ufi pr H20. ee.
  assert (inc x0 (range (graph x2))). wr H14. rw range_inc_rw. ex_tac.
  fct_tac. rwi H22 H23. ufi coarse H23. awi H23. ee. aw. ee. am. app H15.
  app H15. fprops. awi H11. nin H11. nin H12.
  rwi H5 H12. rwi H5 H13. nin (unionf_exists H12). nin (unionf_exists H13). ee.
  assert (exists z, inc z X & inc (P x0) (source z) & inc (Q x0) (source z)).
  cp (Hlc _ _ H14 H15). ufi odr H18. awii H18.
  nin H18; ee; cp (source_extends H20); [exists x2 | exists x1 ]; eee.
  nin H18. clear H14; clear H15; clear H16; clear H17; ee.
  cp (H0 _ H14). ufi ind H17. Ztac. ee. clear H17.
  assert (inc x0 (product (source x3) (source x3))).
  aw. ee; am. ufi pr H19. nin H19. ufi coarse H21. wri H21 H17. awi H17.
  nin H17. cp ((Hg _ H14) _ H17). aw. exists x4. am. fprops. red in H19.
  ee. fprops.
  assert (inc x ind). uf ind. Ztac. uf pr. eee.
  exists x. red. split. aw. ir. cp (H0 _ H13). cp H14. ufi ind H14. Ztac.
  ufi pr H17. ee. uf odr. aw. eee. ufi base H16. bwi H16. ee. red. eee.
  rw H21. fprops.

  nin (Zorn_lemma Hw Hind). red in H. awii H. nin H. cp H.
  assert (binf:is_infinite_c (cardinal (source x))). ufi ind H. Ztac. ufi pr H3.
  ee. assert (sub (source psi) (source x)). red. ir. ufi pr Hprpsi. ee.
  nin H7. nin H7. ee. rwi H11 H6. ufi domain H6. awi H6. nin H6. nin H6.
  cp (H4 _ H6). nin H3. nin H3. ee. rw H16. uf domain. aw. ex_tac.
  cp (sub_smaller H6). red. ee. fprops. nin Hsrcpsi. dneg.
  ap (le_int_is_int H10 H7).

  ufi ind H1. Ztac. ee. set (F:= source x).
  assert (equipotent F (coarse F)). ufi pr H3. uf F. ee. wr H5.
  app equipotent_range.
  set (b:= cardinal F). assert (b = card_mult b b). rw card_mult_pr1.
  assert (cardinal F = cardinal (product b b)). aw. eqtrans (product F F). am.
  app equipotent_product. uf b. fprops. uf b. fprops. ue.
  nin (equal_or_not b E). rw power_x_2. sy. ue. am.
  assert (cardinal_lt b E). red. split.
  assert (sub F E). uf F. ufi base H2. bwi H2. eee. cp (sub_smaller H8).
  uf b. rwii Hb H9. am.
  assert (is_cardinal b). uf b. fprops.
  assert (Hc: card_mult b card_two = card_plus b b).
  rw card_two_pr. rw cardinal_distrib_prod_sum3. rww one_unit_prodr.
  assert (cardinal_le b (card_mult b card_two)). rw Hc. app sum_increasing3.
  assert (cardinal_le (card_mult b card_two) (card_mult b b)).
  app product_increasing2. fprops. fold F in binf. fold b in binf.
  app (finite_le_infinite is_finite2 binf).
  wri H6 H11. cp (cardinal_antisymmetry1 H10 H11).
  assert (cardinal_lt b (cardinal(complement E F))).
  assert (is_cardinal (cardinal (complement E F))). fprops.
  assert (sub F E). uf F. ufi base H2. bwi H2. ee. am.
  cp (cardinal_complement H14). uf b.
  nin (cardinal_le_total_order1 H13 H9). rwi H16 H15. fold b in H15.
  wri Hc H15. wri H12 H15. rwi Hb H15. elim H7. am. nin H16. red in H16.
  ee. assert (cardinal_le b b). fprops.
  cp (sum_increasing2 H18 H16). fold b in H15. rwi H15 H19. wri Hc H19.
  wri H12 H19. rwi Hb H19. co_tac. tv.
  red in H13. ee. red in H13. ee. ufi b H16. wri cardinal_le2 H16. nin H16. ee.
  rename x0 into Y. set (Z:= union2 F Y).
  set (a1:= product F F). set (a2 := product F Y). set (a3 := product Y Z).
  assert (cardinal (union2 a2 a3) = b). rw H12. rw Hc. rw H6.
  app card_plus_pr1. uf a2. uf a3. red. app is_emptyset. red. ir.
  nin (intersection2_both H18).
  awi H19; awi H20. ee. cp (H16 _ H21). srwi H25. ee.
  elim H26. am. uf a2. rw card_mult_pr1. eqtrans (product b b).
  app equipotent_product. uf b. fprops. uf b. eqtrans F. eqsym. am. fprops.
  fprops. uf a3. rw card_mult_pr1. eqtrans (product b b).
  app equipotent_product. uf b. fprops. uf b. eqtrans F. eqsym. am. fprops.
  uf Z. rw H12. rw Hc. wr cardinal_equipotent.
  assert (cardinal (card_plus b b) = (card_plus b b)). rww cardinal_of_cardinal.
  fprops. rw H18. app card_plus_pr1. red. ir. app is_emptyset. ir.
  red; ir. nin (intersection2_both H19).
  cp (H16 _ H21). srwi H22. nin H22. elim H23. am. uf b. fprops.
  eqsym. uf b. eqtrans F. fprops. am. fprops.
  assert (product Z Z = union2 (product F F) (union2 a2 a3)). uf Z.
  uf a2. uf a3. uf Z. set_extens. awi H19. ee.
  nin (union2_or H20). nin (union2_or H21). app union2_first. aw. ee; am.
  app union2_second. app union2_first. aw. ee; am.
  app union2_second. app union2_second. aw. ee; am.
  nin (union2_or H19). awi H20. aw. ee. am. app union2_first. app union2_first.
  nin (union2_or H20). awi H21. aw. ee. am. app union2_first.
  app union2_second. awi H21. aw. ee. am. app union2_second. am.
  assert (disjoint (product F F) (union2 a2 a3)). uf a2. uf a3. uf Z.
  red. app is_emptyset. red. ir. nin (intersection2_both H20).
  awi H21. ee. nin (union2_or H22).
  awi H25. ee. cp (H16 _ H27). srwi H28. ee. elim H29. am.
  awi H25. ee. cp (H16 _ H26). srwi H28. ee. elim H29. am.
  assert (equipotent Y (union2 a2 a3)). wr cardinal_equipotent. rww H18.
  uf b. sy. aw. red in H21. nin H21. ee. clear H1. nin H3. ufi coarse H3.
  set (g:= corresp Z (product E E) (union2 (graph x) (graph x0))).
  assert (Hga: source g = Z). uf g. aw.
  assert (Hgb:graph g = (union2 (graph x) (graph x0))). uf g. aw.
  assert (is_function x0). fct_tac. assert (is_function x). fct_tac.
  assert (Hgd: range (graph g) = coarse (source g)). uf coarse. rw Hga. rw Hgb.
  rw H19. wr H23. nin H21. wr (surjective_pr3 H26). rw range_union2.
  uf F. wrr H3.
  assert (Hhf: target g = product E E). uf g. aw.
  assert (Hge:domain (graph g) = (source g)). rw Hgb. rww domain_union2. aw.
  rw H22. rww Hga.
  assert (sub Z E). uf Z. red. ir. nin (union2_or H26). ufi base H2. bwi H2. ee.
  app H28. cp (H16 _ H27). srwi H28. nin H28. am.
  assert (is_function g). uf g. app is_function_pr. app fgraph_union2.
  fprops. fprops. aw. rw H22. empty_tac. nin (intersection2_both H27).
  set (H16 _ H29). srwi i. nin i. contradiction. wr Hgb. rw Hgd. uf coarse.
  fprops. rw Hga. app product_monotone. wr Hgb. ue.

  assert (forall a b c, inc (J a b) (graph x) -> inc (J c b) (graph x0) ->
    False). ir. assert (inc b0 (range (graph x))). aw. ex_tac. fprops.
  assert (inc b0 (range (graph x0))). aw. ex_tac. fprops.
  elim (emptyset_pr (x:= b0)). wr H20. app intersection2_inc.
  uf F. wrr H3. wr H23. nin H21. wr (surjective_pr3 H32). am.
  assert (injective g). app injective_pr_bis. simpl. uf related.
  rw Hgb. ir. nin (union2_or H29); nin (union2_or H30).
  ap (injective_pr3 H1 H31 H32). elim (H28 _ _ _ H31 H32).
  elim (H28 _ _ _ H32 H31). nin H21. ap (injective_pr3 H21 H31 H32).
  assert (inc g ind). clear H1. uf ind. Ztac. uf base. bw. eee. uf g. aw.
  uf pr. eee. apw sub_trans (graph x). app union2sub_first.
  assert (gle (induced_order odr ind) x g). aw. uf odr.
  rw extension_order_pr2. bw. ufi base H2. bwi H2. eee. app union2sub_first.
  cp (H0 _ H31). set (f_equal source H32). rwi Hga e. ufi Z e.
  assert (Y= emptyset). app is_emptyset. red. ir. cp (H16 _ H33). srwi H34.
  ee. elim H35. uf F. wr e. app union2_second.
  assert (cardinal Y = card_zero). rw H33. fprops.
  assert (cardinal F = card_zero). wr H34. aw.
  nin binf. nin H37. ufi F H35. rw H35. fprops.
Qed.

Lemma power_of_infinite: forall a n, is_infinite_c a -> inc n Bnat ->
  n <> card_zero -> card_pow a n = a.
Proof. ir. rwi inc_Bnat H0. cp (predc_pr H0 H1). ee. rw H3.
  set (m:= predc n) in *. wri inc_Bnat H0.
  assert (is_cardinal a). red in H; ee;am.
  app (cardinal_c_induction_v (fun m=> card_pow a (succ m) = a)).
  rw succ_zero. app power_x_1. ir. uf succ.
  rw power_of_sum2. ufi succ H6. rw H6. rw power_x_1. wr power_x_2.
  app equipotent_inf2_inf. am. am. bw.
Qed.

Lemma finite_family_product: forall a f, fgraph f ->
  is_finite_set (domain f) -> is_infinite_c a ->
  (forall i, inc i (domain f) -> cardinal_le (V i f) a) ->
  (forall i, inc i (domain f) -> V i f <> card_zero) ->
  (exists j, inc j (domain f) & (V j f) = a) ->
  cardinal_prod f = a.
Proof. ir. set (g:= cst_graph (domain f) a).
  assert (fgraph g). uf g. uf cst_graph. gprops.
  assert (domain f = domain g). uf g. uf cst_graph. bw.
  assert (forall x, inc x (domain f) -> cardinal_le (V x f) (V x g)).
  ir. uf g. uf cst_graph. bw. app H2.
  cp (product_increasing H H5 H6 H7). ufi g H8. rwi card_pow_pr2 H8.
  assert (nonempty (domain f)). nin H4. ee. exists x. am.
  set (n:= cardinal (domain f)). assert (inc n Bnat). bw.
  assert (n <> card_zero). uf n. app cardinal_nonemptyset1.
  assert (card_pow a (domain f) = card_pow a n). uf n. app card_pow_pr.
  fprops. fprops. rwi (power_of_infinite H1 H10 H11) H12. rwi H12 H8.
  nin H4. ee. rename x into j0. set (j:= singleton j0).
  assert (forall x, inc x (domain f) -> is_cardinal (V x f)). ir.
  cp (H7 _ H14). red in H15; ee; am. assert (sub j (domain f)). red. ir.
  ufi j H15. rw (singleton_eq H15). am.
  cp (product_increasing1 H H14 H3 H15). ufi j H16.
  rwi trivial_cardinal_prod3 H16. rwi H13 H16. co_tac.
  am. am. rw H13. red in H1; ee; am.
Qed.

Lemma product2_infinite: forall a b, cardinal_le b a ->
  is_infinite_c a -> b <> card_zero -> card_mult a b = a.
Proof. ir. assert (is_cardinal a). red in H; ee; am.
  assert (is_cardinal b). red in H; ee; am.
  assert (cardinal_le (card_mult a b) (card_mult a a)).
  app product_increasing2. fprops. wri power_x_2 H4.
  rwi equipotent_inf2_inf H4.
  assert (cardinal_le a (card_mult a b)). app product_increasing3. co_tac.
  am. am.
Qed.

Lemma notbig_family_sum: forall a f, fgraph f ->
  is_infinite_c a -> cardinal_le (cardinal (domain f)) a ->
  (forall i, inc i (domain f) -> cardinal_le (V i f) a) ->
  cardinal_le (cardinal_sum f) a.
Proof. ir. assert (Ha: is_cardinal a). red in H0; ee; am.
  nin (emptyset_dichot (domain f)).
  rww trivial_cardinal_sum. app zero_smallest.
  set (b := cardinal (domain f)) in *. assert (Hb:b <> card_zero).
  uf b. app cardinal_nonemptyset1. clear H3.
  set (g:= L (domain f) (fun _ =>a)).
  assert (fgraph g). uf g. gprops. assert (domain f = domain g). uf g. bw.
  assert (forall x, inc x (domain f) -> cardinal_le (V x f) (V x g)).
  ir. uf g. bw. app H2. cp (sum_increasing H H3 H4 H5). ufi g H6.
  assert (L (domain f) (fun _ : Set => a) = cst_graph (domain f) a). tv.
  rwi H7 H6. rwi sum_of_same1 H6. cut (card_mult a (domain f) = a). ir.
  wrr H8. assert (card_mult a b = a). app product2_infinite. wr H8.
  app card_mult_pr2. rww H8. uf b. aw. fprops.
Qed.

Lemma notbig_family_sum1: forall a f, fgraph f ->
  is_infinite_c a -> cardinal_le (cardinal (domain f)) a ->
  (forall i, inc i (domain f) -> cardinal_le (V i f) a) ->
  (exists j, inc j (domain f) & (V j f) = a) ->
  (cardinal_sum f) = a.
Proof. ir. cp (notbig_family_sum H H0 H1 H2). nin H3. nin H3.
  assert (sub (singleton x) (domain f)). red. ir. rw (singleton_eq H6). am.
  assert (forall x, inc x (domain f) -> is_cardinal (V x f)). ir.
  cp (H2 _ H7). red in H8; ee; am.
  cp (sum_increasing1 H H7 H6). rwi trivial_cardinal_sum3 H8. rwi H5 H8.
  co_tac. am. am. rw H5. red in H0; ee; am.
Qed.

Lemma sum2_infinite: forall a b, cardinal_le b a ->
  is_infinite_c a -> card_plus a b = a.
Proof. ir. assert (is_cardinal a). red in H; ee; am.
  assert (is_cardinal b). red in H; ee; am.
  assert (cardinal_le (card_plus a b) (card_plus a a)).
  app sum_increasing2. fprops.
  assert (card_plus a a = card_mult a card_two). rw card_two_pr.
  rw cardinal_distrib_prod_sum3. rww one_unit_prodr. rwi product2_infinite H4.
  assert (cardinal_le a (card_plus a b)). app sum_increasing3.
  rwi H4 H3. co_tac.
  app (finite_le_infinite is_finite2 H0). am. app card_two_not_zero.
Qed.

Lemma cardinal_comp_singl_inf: forall E x,
  infinite_set E -> cardinal E = cardinal (complement E (singleton x)).
Proof. ir. nin (p_or_not_p (inc x E)). ir.
  cp (cardinal_succ_pr1 E x). wri tack_on_complement H1.
  nin H. ee. rwi H1 H2. wri is_finite_succ H2.
  set (F:=(complement E (singleton x))) in *.
  assert (is_infinite_c (cardinal F)). red. split. fprops. am.
  rw H1. sy. ufi is_finite_c H2.
  ex_middle. elim H2.
  split. fprops. am. fprops. am.
  ir. assert (E=complement E (singleton x)). set_extens. rw inc_complement.
  split. am. red. ir. elim H0. wrr (singleton_eq H2). rwi inc_complement H1.
  nin H1; am. wrr H1.
Qed.

EIII-6-4 Countable sets

Definition is_countable_set E:= equipotent_to_subset E Bnat.

Lemma countable_prop: forall E,
  is_countable_set E = cardinal_le (cardinal E) (cardinal Bnat).
Proof. ir. uf cardinal_le. uf is_countable_set. ap iff_eq. ir. ee.
  fprops. fprops. wrr cardinal_le2. ir. ee. rww cardinal_le2.
Qed.

Lemma infinite_greater_countable1: forall E,
  infinite_set E -> cardinal_le (cardinal Bnat) (cardinal E).
Proof. ir. nin (infinite_greater_countable H). nin H0. wr H1.
  app sub_smaller.
Qed.

Lemma countable_finite_or_N: forall E, is_countable_set E ->
  is_finite_c (cardinal E) \/ cardinal E = cardinal Bnat.
Proof. ir. rwi countable_prop H.
  nin (p_or_not_p (is_finite_c (cardinal E))).
  ir. au. ir. right. assert (infinite_set E). red. red. split.
  fprops. am. cp (infinite_greater_countable1 H1). co_tac.
Qed.

Lemma countable_finite_or_N_b: forall E, is_countable_set E ->
  is_finite_set E \/ equipotent E Bnat.
Proof. ir. nin (countable_finite_or_N H). left. am. right. awi H0. am.
Qed.

Lemma countable_finite_or_N_c: forall E, is_countable_set E ->
  infinite_set E -> equipotent E Bnat.
Proof. ir. nin (countable_finite_or_N_b H). red in H0; red in H1. ee.
  red in H0. ee. elim H2. am. am.
Qed.

Theorem countable_subset: forall E F, sub E F -> is_countable_set F ->
  is_countable_set E.
Proof. ir. rw countable_prop. rwi countable_prop H0.
  apply cardinal_le_transitive with (cardinal F). app sub_smaller. am.
Qed.

Theorem countable_product: forall f, fgraph f ->
  is_finite_set (domain f) ->
  (forall i, inc i (domain f) -> is_countable_set (V i f)) ->
  is_countable_set (productb f).
Proof. ir. rw countable_prop.
  set (g:= L(domain f) (fun i => cardinal (V i f))).
  assert (cardinal (productb f) = cardinal_prod g). rw cardinal_prod_pr. tv.
  am. rw H2. set (h:= L(domain f)(fun i:Set => cardinal Bnat)).
  apply cardinal_le_transitive with (cardinal_prod h).
  app product_increasing. uf g. gprops. uf h. gprops. uf g; uf h; bw. uf g.
  uf h. bw. ir. bw. cp (H1 _ H3). rwi countable_prop H4. am.
  assert (h = cst_graph (domain f) (cardinal Bnat)). tv. rw H3.
  rw card_pow_pr2. red in H0. set (cf := cardinal (domain f)) in *.
  set (cb:= (cardinal Bnat)) in *.
  assert (card_pow cb (domain f) = card_pow cb (cardinal (domain f))).
  app card_pow_pr. fprops. fprops. rw H4. fold cf.
  nin (equal_or_not cf card_zero). rw H5. rw power_x_0.
  app one_small_cardinal. uf cb. fprops. red. ir. cp infinite_Bnat.
  red in H7. ee. elim H8. ufi cb H6. rw H6. wr inc_Bnat. fprops.
  rw power_of_infinite. uf cb. fprops. uf cb. ap infinite_Bnat. bw. am.
Qed.

Theorem countable_union: forall f, fgraph f ->
  is_countable_set (domain f) ->
  (forall i, inc i (domain f) -> is_countable_set (V i f)) ->
  is_countable_set (unionb f).
Proof. ir. rw countable_prop.
  set (g:= L(domain f) (fun i => cardinal (V i f))).
  apply cardinal_le_transitive with (cardinal_sum g). uf g.
  app cardinal_sum_pr1.
  set (h:= L(domain f)(fun i:Set => cardinal Bnat)).
  apply cardinal_le_transitive with (cardinal_sum h).
  app sum_increasing. uf g. gprops. uf h. gprops. uf g; uf h; bw. uf g. uf h.
  bw. ir. bw. cp (H1 _ H2). rwi countable_prop H3. am.
  assert (Ha:h = cst_graph (domain f) (cardinal Bnat)). tv. rw Ha.
  rw sum_of_same1. rwi countable_prop H0. set (cb:= (cardinal Bnat)) in *.
  assert (card_mult cb (domain f) = card_mult cb (cardinal (domain f))).
  app card_mult_pr2. sy. fprops. rw H2.
  apply cardinal_le_transitive with (card_mult cb cb). app product_increasing2.
  uf cb. fprops. wr power_x_2.
  uf cb. rw (equipotent_inf2_inf infinite_Bnat). fprops. uf cb. fprops.
Qed.

Theorem infinite_partition: forall E, infinite_set E ->
  exists f, partition_fam f E & equipotent (domain f) E &
    (forall i, inc i (domain f) -> (infinite_set (V i f) &
      is_countable_set (V i f))).
Proof. ir. cp (infinite_greater_countable1 H).
  assert (cardinal Bnat <> card_zero). red. ir.
  cp (cardinal_nonemptyset H1). assert (inc card_zero emptyset). wr H2.
  fprops. elim (emptyset_pr H3). cp (product2_infinite H0 H H1).
  rwi card_mult_pr1 H2. awi H2. red in H2. nin H2. ee.
  set (f:= L (cardinal E) (fun a => image_by_fun x
    (product (singleton a) (cardinal Bnat)))). nin H2.
  assert (Ha:is_graph (graph x)). red in H2. ee. fprops.
  assert (fgraph f). uf f. gprops. exists f. ee. red. ee. am.
  app mutually_disjoint_prop. ir. ufi f H9; ufi f H10. bwi H9; bwi H10.
  ufi image_by_fun H9. ufi image_by_fun H10. awi H9. awi H10.
  nin H9; nin H10. ee. awi H9; awi H10. ee. red in H12. red in H11.
  cp (injective_pr3 H2 H12 H11). wr H13.
  wrr H15. rww H17. red in H2; ee. fprops.
  red in H2; ee. fprops. ufi f H8; bwi H8. am. ufi f H7; bwi H7. am.
  ufi f H8; bwi H8. am. wr H4. uf f. uf image_by_fun. set_extens.
  rwi unionb_rw H7. nin H7. bwi H7. ee. awi H8. nin H8.
  ee. red in H2; ee. red in H2; ee. ap (corresp_sub_range H2). ex_tac.
  nin H7; am. red in H5. ee.
  wri H8 H7. ufi image_of_fun H7. awi H7. nin H7. ee. rwi H3 H7. awi H7.
  ee. rw unionb_rw. exists (P x1). bw. split. am. aw. exists x1. split.
  aw. intuition. am. uf f. bw. fprops. ir. uf f. bw. ir.
  set (dom:= (product (singleton i) (cardinal Bnat))).
  ufi f H7. bwi H7. assert (sub dom (source x)). rw H3. uf dom. red. ir.
  awi H8. ee. aw. ee. am. rww H9. am.
  assert (bijective x). split;am. cp (equipotent_restriction H8 H9).
  assert (equipotent dom Bnat). uf dom. eqtrans (cardinal Bnat).
  eqtrans (product (cardinal Bnat) (singleton i)).
  app equipotent_product_sym. eqsym. app equipotent_prod_singleton. fprops.
  assert (equipotent (image_by_fun x dom) Bnat). eqtrans dom. eqsym. am. am.
  split. red. wri cardinal_equipotent H12. rw H12. app infinite_Bnat. red.
  red. exists Bnat. split. fprops. am. ufi f H7. bwi H7. am.
Qed.

Lemma countable_inv_image: forall f, surjective f ->
  (forall y, inc y (target f) ->
    is_countable_set (inv_image_by_fun f (singleton y))) ->
  infinite_set (target f) ->
  equipotent (source f) (target f).
Proof. ir. rename H1 into Hc. assert (Ha: is_function f). nin H. am.
  set (pa := L (target f) (fun z=> (inv_image_by_fun f (singleton z)))).
  assert (unionb pa = (source f)). set_extens. ufi pa H1. rwi unionb_rw H1.
  nin H1. ee. bwi H1. bwi H2. ufi inv_image_by_fun H2. awi H2. nin H2.
  ee. rwi (singleton_eq H2) H3. graph_tac. am.
  uf pa. rw unionb_rw. exists (W x f). cp (inc_W_target Ha H1).
  bw. ee. am. uf inv_image_by_fun. aw. ex_tac. app W_pr3.
  assert (mutually_disjoint pa). app mutually_disjoint_prop. uf pa. bw.
  uf inv_image_by_fun. ir. bwi H4; bwi H5. awi H4. awi H5. nin H4. nin H5. ee.
  wr (singleton_eq H4). wrr (singleton_eq H5).
  assert (fgraph (graph f)). fprops. red in H8. ee.
  red in H7. red in H6. assert (P (J y x) = P (J y x0)). aw.
  cp (H9 _ _ H7 H6 H10). ap (pr2_def H11). fprops. fprops. am.
  assert (fgraph pa). uf pa. gprops.
  cp (cardinal_sum_pr H3).
  ufi disjoint_union H4.
  assert (equipotent (unionb (disjoint_union_fam pa)) (unionb pa)).
  app equipotent_disjoint_union. uf pa. gprops.
  uf disjoint_union_fam. gprops. uf disjoint_union_fam. bw. ir.
  uf disjoint_union_fam. bw. eqsym. app equipotent_prod_singleton.
  ufi disjoint_union_fam H5. bwi H5. am. app disjoint_union_disjoint.
  wri cardinal_equipotent H5. rwi H4 H5. rwi H1 H5.
  set (g:= L (domain pa) (fun _:Set => cardinal Bnat)).
  set (cf:= L (domain pa) (fun a : Set => cardinal (V a pa))).
  assert (cardinal_le (cardinal_sum cf) (cardinal_sum g)).
  app sum_increasing. uf cf. gprops. uf g. gprops. uf cf; uf g; bw.
  uf cf; uf g. bw. ir. bw. ufi pa H6. bwi H6. cp (H0 _ H6).
  rwi countable_prop H7. uf pa. bw.
  assert (Hd:g = cst_graph (domain pa) (cardinal Bnat)). tv. rwi Hd H6.
  rwi sum_of_same1 H6.
  ufi pa H6. bwi H6. fold cf in H5. rwi H5 H6.
  assert (card_mult (cardinal Bnat) (target f) = cardinal (target f)).
  transitivity (card_mult (cardinal Bnat) (cardinal (target f))).
  app card_mult_pr2. aw. fprops. set (u:= cardinal (target f)).
  rw card_mult_commutative. app product2_infinite. uf u.
  app infinite_greater_countable1. red. ir.
  cp infinite_Bnat. rwi H7 H8. red in H8. nin H8. elim H9. app is_finite0.
  assert (cardinal_le (cardinal (target f)) (cardinal (source f))).
  app surjective_cardinal_le. exists f. ee. am. tv. tv.
  rwi H7 H6. cp (cardinal_antisymmetry1 H6 H8). awi H9. am.
Qed.

Theorem infinite_finite_subsets: forall E, infinite_set E ->
  equipotent (Zo (powerset E) (fun z => is_finite_set z)) E.
Proof. ir. set (bF:=Zo (powerset E) (fun z : Set => is_finite_set z)).
  set (T:=fun n => Zo (powerset E) (fun z => cardinal z = n)).
  assert (forall n, inc n Bnat -> cardinal_le (cardinal (T n)) (cardinal E)).
  ir. assert (cardinal n = n). fprops.
  set (K:= Zo(set_of_functions n E)(fun z => injective z)).
  set (f:= BL (fun z => range (graph z)) K (T n)).
  assert (transf_axioms (fun z => range (graph z)) K (T n)). red. uf K; uf T.
  ir. Ztac. awi H3. ee. clear H2. Ztac. aw. wr H6. nin H3; fprops.
  wr H1. sy. aw. awi H3. ee. wr H5. app equipotent_range.
  assert (is_function f). uf f. app bl_function.
  set (q:= set_of_permutations n). set (c := cardinal q).
  assert (is_finite_c c). uf c. uf q. cp (nat_to_B_pr H0).
  assert (cardinal n = nat_to_B (cardinal_nat n)). rw H1. sy; am.
  cp (number_of_permutations _ H5). rw H6. wr inc_Bnat. fprops.
  assert (forall x, inc x (target f) ->
    cardinal (inv_image_by_fun f (singleton x))=c). ir. uf c. aw.
  ufi f H5. awi H5. ufi T H5. Ztac. clear H5.
  assert (equipotent n x). symmetry in H7. wri H1 H7. awi H7. am. nin H5. ee.
  set (x1:= corresp n E (graph x0)).
  assert (source x1 = n). uf x1. aw.
  assert (target x1 = E). uf x1. aw.
  assert (injective x1). app injective_pr_bis. uf x1. nin H5. nin H12.
  app is_function_pr. fprops. apw sub_trans (target x0). nin H12. fprops. ue.
  awi H6. am. aw. sy; am. uf x1. aw. nin H5. ir. ap (injective_pr H5 H13 H14).
  set(iif := inv_image_by_fun f (singleton x)).
  set (g:= BL (fun z=> (compose x1 z)) q iif).
  assert (transf_axioms (fun z=> (compose x1 z)) q iif).
  uf q; uf iif. red. ir. ufi set_of_permutations H13. Ztac.
  clear H13. uf inv_image_by_fun. aw. ex_tac. awi H14. ee.
  assert (composable x1 c0). red. ee. fct_tac. am. ue.
  set (t:= compose x1 c0). assert (is_function t). uf t. fct_tac.
  assert (inc t K). uf K. Ztac. aw. ee. am. uf t. aw. uf t. aw. uf t.
  app inj_compose1. nin H15. am. ue.
  assert (x = W t f). uf f. aw. uf t. uf compose. aw.
  rw compose_range. assert (range (graph c0) = n).
  red in H15. ee. rw (surjective_pr3 H20). am. rw H20. uf x1.
  nin H5. nin H21. ufi image_of_fun H22. wr H8. aw. rw H22. sy; am. fprops.
  rw H20. app W_pr3. uf f. aw.
  assert (is_function g). uf g. app bl_function.
  eqsym. exists g. ee; tv; uf g; aw.
  app bl_bijective. uf q. uf set_of_permutations.
  ir. Ztac. clear H16. Ztac. awi H18; awi H16. ee. app function_exten.
  ue. ue. ir. assert (W x2 (compose x1 u) = W x2 (compose x1 v)).
  ue. awi H26. red in H12. ee. app H27. rw H10. wr H22. app inc_W_target.
  rw H10. wr H24. app inc_W_target. rw H23. wrr H21. red. ee. fct_tac.
  am. rww H24. rw H23. wr H21. am. red. ee. fct_tac. am. rw H22. am. am.
  uf iif. uf q. ir. ufi inv_image_by_fun H15. awi H15. nin H15. ee.
  rwi (singleton_eq H15) H16. clear H15. cp (inc_pr1graph_source H3 H16).
  cp (W_pr H3 H16). ufi f H17. rwii bl_W H17. ufi f H15. awi H15.
  ufi K H15. Ztac. clear H15. awi H18. ee.
  wri H11 H20. cp (exists_right_composable H15 H12 H20). rwi H17 H21.
  assert (x = (range (graph x1))). uf x1. aw. nin H5. rw (surjective_pr3 H22).
  sy. am. assert (sub x (range (graph x1))). rw H22. fprops. nin H5.
  wri H21 H23. nin H23. nin H23. exists x3.
  assert (source x3 = n). wr H18. wr H25. aw.
  assert (target x3 = n). red in H23. ee. wrr H28.
  assert (surjective x3). app surjective_pr5. red in H23; ee; am. rw H27.
  ir. set (u:= W y0 x1). assert (inc u x). rw H22. aw. exists y0.
  uf u. app W_pr3. nin H12. am. ue. nin H12. ee. fprops.
  wri H17 H29. wri H25 H29. awi H29. nin H29. ufi compose H29. awi H29.
  nin H29. nin H30. ee. nin H12. cp (W_pr H12 H31). exists x4. split.
  red in H23. ee. ap (inc_pr1graph_source H34 H30). red. assert (x5 = y0).
  app H32. ap (inc_pr1graph_source H12 H31). ue. ue. rw H25. fprops.
  split. uf set_of_permutations. Ztac. aw. eee. fct_tac.
  app bijective_if_same_finite_c_surj. rw H26; rw H27; tv.
  rw H26. red. rw H1. wr inc_Bnat. am. tv. ufi f H15. awi H15. am.
  cp (shepherd_principle H3 H5). ufi f H6. awi H6.
  nin (equal_or_not n card_zero). rw H7.
  assert (cardinal (T card_zero) = card_one).
  assert (T card_zero = singleton emptyset). uf T. set_extens. Ztac.
  rw (cardinal_nonemptyset H10). fprops. rw (singleton_eq H8). Ztac.
  app powerset_inc. app emptyset_sub_any. app cardinal_zero.
  rw H8. app cardinal_singleton. rw H8.
  app finite_le_infinite. app is_finite1.
  nin (p_or_not_p (is_finite_c (cardinal (T n)))). ir.
  app finite_le_infinite. ir.
  set (K1:= cardinal (set_of_functions n E)).
  assert (K1 = cardinal E). uf K1. change (card_pow E n = cardinal E).
  assert (card_pow E n = card_pow (cardinal E) n). app card_pow_pr.
  fprops. fprops. rw H9. app power_of_infinite.
  assert (cardinal_le (cardinal K) (cardinal E)). wr H9. uf K1.
  app sub_smaller. uf K. app Z_sub.
  apply cardinal_le_transitive with (cardinal K). rw H6.
  assert (is_infinite_c (cardinal (T n))). red. ee. fprops. am.
  assert (cardinal_le c (cardinal (T n))). app finite_le_infinite.
  assert (c <> card_zero). uf c. uf q.
  cp (nat_to_B_pr H0).
  assert (cardinal n = nat_to_B (cardinal_nat n)). rw H13. am.
  rw (number_of_permutations _ H14). wr nat_B_0. red. ir.
  cp (nat_B_inj _ _ H15). elim (factorial_nonzero (cardinal_nat n)). sy; am.
  cp (product2_infinite H12 H11 H13). rw H14. fprops. am.
  rename H0 into Haux.
  set (Fn := L Bnat (fun n => Zo (powerset E) (fun z => cardinal z = n))).
  assert (bF = unionb Fn). uf bF; uf Fn; set_extens. Ztac. clear H0.
  rw unionb_rw. bw. exists (cardinal x). split. rw inc_Bnat. am. bw. Ztac.
  rw inc_Bnat. am. rwi unionb_rw H0. bwi H0. nin H0. nin H0. bwi H1. Ztac.
  clear H1. Ztac. red. rw H3. wrr inc_Bnat. am.
  assert (equipotent (unionb (disjoint_union_fam Fn)) (unionb Fn)).
  app equipotent_disjoint_union. uf Fn. uf disjoint_union_fam. gprops.
  uf Fn. gprops. uf disjoint_union_fam. bw. uf disjoint_union_fam. bw. ir.
  bw. eqsym. app equipotent_prod_singleton. app disjoint_union_disjoint.
  uf Fn. gprops. app mutually_disjoint_prop. uf Fn. bw. ir. bwi H4. bwi H3.
  Ztac. clear H4. Ztac. wrr H7. am. am.
  wri cardinal_equipotent H1. wri H0 H1.
  assert (fgraph Fn). uf Fn. gprops. cp (cardinal_sum_pr H2).
  ufi disjoint_union H3. rwi H1 H3. clear H1.
  assert (cardinal_le (cardinal_sum (L (domain Fn)(fun a => cardinal (V a Fn))))
    (cardinal_sum (L (domain Fn) (fun a : Set => cardinal E)))).
  app sum_increasing. gprops. gprops. bw. bw. ir. bw. ufi Fn H1. bwi H1.
  ufi T Haux. uf Fn. bw. app Haux. bw. bw. wri H3 H1.
  assert (Hx:L (domain Fn) (fun _ : Set => cardinal E) = cst_graph (domain Fn)
    (cardinal E)). tv. rwi Hx H1. rwi sum_of_same1 H1.
  assert (card_mult (cardinal E) (domain Fn) = cardinal E). uf Fn. bw.
  assert (card_mult (cardinal E)Bnat = card_mult (cardinal E) (cardinal Bnat)).
  app card_mult_pr2. sy. fprops. rw H4. app product2_infinite.
  app infinite_greater_countable1. red. ir. cp (cardinal_nonemptyset H5).
  assert (inc card_zero emptyset). wr H6. fprops. elim (emptyset_pr H7).
  rwi H4 H1. clear H4.
  assert (cardinal_le (cardinal E) (cardinal bF)). wr cardinal_le3.
  rw cardinal_le1. exists (BL (fun x => singleton x) E bF). ee.
  app bl_injective. red. uf bF. ir. Ztac. app powerset_inc. red. ir.
  rww (singleton_eq H5). red. rw cardinal_singleton. app is_finite1.
  ir. app singleton_inj. aw. aw.
  cp (cardinal_antisymmetry1 H1 H4). awi H5. am.
Qed.

Lemma infinite_finite_sequence: forall E, infinite_set E ->
 equipotent (Zo(set_of_sub_functions Bnat E) (fun z=> is_finite_set (source z)))
 E.
Proof. ir. set (q:= Zo (set_of_sub_functions Bnat E)
  (fun z => is_finite_set (source z))).
  assert (Ha:cardinal_le (cardinal q) (cardinal E)).
  assert (infinite_set Bnat). red. ap (infinite_Bnat).
  cp (infinite_finite_subsets H0).
  set (Fn:=Zo (powerset Bnat) (fun z => is_finite_set z)) in H1.
  assert(q = unionb (L Fn (fun z=> (set_of_functions z E)))).
  uf q. uf Fn. set_extens. Ztac. clear H2. bwi H3.
  ee. assert (inc (source x) (Zo (powerset Bnat) (fun z => is_finite_set z))).
  Ztac. aw.
  apply unionb_inc with (source x). bw. bw. aw. eee. rwi unionb_rw H2.
  nin H2. bwi H2. nin H2. Ztac. awi H3. bw. eee. awi H4. am. awi H3. ee. ue.
  nin H2. am.
  assert(forall z, inc z Fn -> cardinal_le
    (cardinal (set_of_functions z E)) (cardinal E)).
  ir. change (cardinal_le (card_pow E z) (cardinal E)).
  ufi Fn H3. Ztac. red in H5.
  assert (card_pow E z = card_pow (cardinal E) (cardinal z)).
  app card_pow_pr. fprops. fprops. rw H6.
  assert (is_infinite_c (cardinal E)). am.
  assert (inc (cardinal z) Bnat). rw inc_Bnat. am.
  nin (equal_or_not (cardinal z) (card_zero)). rw H9. rw power_x_0.
  app finite_le_infinite. app is_finite1.
  cp (power_of_infinite H7 H8 H9). rw H10. fprops.
  assert (fgraph (L Fn (fun z : Set => set_of_functions z E))). gprops.
  cp (cardinal_sum_pr1 H4). fold q in H5. wri H2 H5. bwi H5.
  set (g:= (L Fn (fun _:Set => cardinal E))).
  set (f0:= (L Fn (fun a =>
    cardinal (V a (L Fn (fun z : Set => set_of_functions z E)))))) in *.
  assert (fgraph f0). uf f0. gprops. assert (fgraph g). uf g. gprops.
  assert (domain f0 = domain g). uf f0. uf g. bw.
  assert (forall x, inc x (domain f0) -> cardinal_le (V x f0) (V x g)).
  uf f0; uf g. bw. ir. bw. app H3.
  cp (sum_increasing H6 H7 H8 H9).
  apply cardinal_le_transitive with (cardinal_sum f0). am.
  cut(cardinal E = cardinal_sum g). ir. rww H11.
  assert (Hx:g= cst_graph Fn (cardinal E)). uf g. tv. rw Hx. rw sum_of_same1.
  assert (card_mult (cardinal E) Fn = card_mult (cardinal E) (cardinal Fn)).
  app card_mult_pr2. sy. fprops. rw H11.
  cp (infinite_greater_countable1 H).
  assert (cardinal Fn = cardinal Bnat). aw. rw H13. red in H.
  assert (cardinal Bnat <> card_zero). app cardinal_nonemptyset1.
  cp (inc0_Bnat). exists card_zero. am.
  sy. ap (product2_infinite H12 H H14).
  assert (cardinal_le (cardinal E) (cardinal q)).
  set (f0:= fun z:Set => (fun _:Set => z)).
  assert (Hb: forall z, inc z E-> transf_axioms (f0 z)(singleton card_zero) E).
  red. ir. awi H1. rw H1. uf f0. am.
  assert (forall z, inc z E -> is_function (BL (f0 z)(singleton card_zero) E)).
  ir. app bl_function. app Hb.
  set (f1:= fun z => (BL (f0 z)(singleton card_zero) E)).
  assert (forall z, inc z E -> inc (f1 z) q). ir. uf q. Ztac.
  bw. uf f1. ee. app H0. aw. red. ir. awi H2. rw H2.
  fprops. aw. aw. uf f1. aw. red. rw cardinal_singleton. wr inc_Bnat.
  fprops. set (f:= BL f1 E q). assert (injective f). uf f.
  app bl_injective. ir. cp (f_equal (W card_zero) H4). ufi f1 H5.
  assert (inc card_zero (singleton card_zero)). fprops. awii H5.
  app Hb. app Hb. wr cardinal_le3. rw cardinal_le1.
  exists f. ee. am. uf f. aw. uf f. aw.
  cp (cardinal_antisymmetry1 Ha H0). awi H1. am.
Qed.

EIII-6-5 Stationary sequences


Definition stationary_sequence f :=
  fgraph f & domain f = Bnat &
  exists m, inc m Bnat & forall n, inc n Bnat -> cardinal_le m n ->
    V n f = V m f.

Definition increasing_sequence f r:=
  fgraph f & domain f = Bnat & sub (range f) (substrate r) &
  forall n m, inc n Bnat -> inc m Bnat -> cardinal_le n m ->
    gle r (V n f) (V m f).

Definition decreasing_sequence f r:=
  fgraph f & domain f = Bnat & sub (range f) (substrate r) &
  forall n m, inc n Bnat -> inc m Bnat -> cardinal_le n m ->
    gle r (V m f) (V n f).

Lemma increasing_prop: forall f r, order r ->
  is_function f -> source f = Bnat -> sub (target f) (substrate r) ->
  (forall n, inc n Bnat -> gle r (W n f) (W (succ n) f)) ->
  increasing_sequence (graph f) r.
Proof. ir. red. ee. fprops. red in H0. ee. wrr H5.
  apply sub_trans with (target f). nin H0. fprops. am.
  ir. cp (card_sub_pr H5 H4 H6). wr H7. set (q:= card_sub m n).
  change (gle r (W n f) (W (card_plus n q) f)).
  assert (forall q, inc q Bnat -> gle r (W n f) (W (card_plus n q) f)).
  app cardinal_c_induction_v. rw zero_unit_sumr. order_tac.
  app H2. app inc_W_target. rww H1. fprops. ir.
  assert (card_plus n (succ n0) = succ (card_plus n n0)). uf succ.
  rww card_plus_associative. rw H10.
  assert (inc (card_plus n n0) Bnat). fprops.
  cp (H3 _ H11). order_tac. app H8. uf q. fprops.
Qed.

Lemma decreasing_prop: forall f r, order r ->
  is_function f -> source f = Bnat -> sub (target f) (substrate r) ->
  (forall n, inc n Bnat -> gge r (W n f) (W (succ n) f)) ->
  decreasing_sequence (graph f) r.
Proof. ir. red. ee. fprops. red in H0. ee. wrr H5.
  apply sub_trans with (target f). nin H0. fprops. am.
  ir. cp (card_sub_pr H5 H4 H6). wr H7. set (q:= card_sub m n).
  change (gge r (W n f) (W (card_plus n q) f)).
  assert (forall q, inc q Bnat -> gge r (W n f) (W (card_plus n q) f)).
  app cardinal_c_induction_v. rw zero_unit_sumr.
  red. order_tac. app H2. app inc_W_target. rww H1. fprops. ir.
  assert (card_plus n (succ n0) = succ (card_plus n n0)). uf succ.
  rww card_plus_associative. rw H10. red in H9. red.
  assert (inc (card_plus n n0) Bnat). fprops.
  cp (H3 _ H11). red in H12. order_tac. app H8. uf q. fprops.
Qed.

Theorem increasing_stationary: forall r, order r ->
  (forall X, sub X (substrate r) -> nonempty X ->
     exists a, maximal_element (induced_order r X) a) =
  (forall f, increasing_sequence f r -> stationary_sequence f).
Proof. ir. app iff_eq. ir. red in H1. ee. assert (Ha: is_graph f). fprops.
  assert (nonempty (range f)). exists (V card_zero f). aw. exists card_zero.
  app fdomain_pr1. rw H2. fprops. nin (H0 _ H3 H5).
  nin H6. awi H6. nin H6. assert (inc x0 Bnat). wr H2. aw. exists x. am.
  red. ee. am. am. exists x0. split. am. ir.
  cp (H4 _ _ H8 H9 H10). cp (pr2_V H1 H6). awi H12. wr H12. app H7.
  aw. rww H12. exists x0. am.
  exists n. app fdomain_pr1. rww H2. am. am. am.
  ir. set (T:= fun x => Zo X (fun y => glt r x y)).
  nin (emptyset_dichot (productb (L X T))). ir.
  assert (exists x, inc x X & T x = emptyset). app exists_proof. red. ir.
  assert (fgraph (L X T)). gprops.
  assert (forall i, inc i (domain (L X T)) -> nonempty (V i (L X T))).
  ir. bw. nin (emptyset_dichot (T i)). elim (H4 i). split. bwi H6. am. am.
  am. bwi H6. am. cp (product_nonempty H5 H6). rwi H3 H7. nin H7.
  elim (emptyset_pr H7).
  ufi T H4. nin H4. exists x. red. aw. split. ee. am. ir.
  ex_middle. nin H4. empty_tac1 x0.
  Ztac. assert (inc x0 (substrate (induced_order r X))). order_tac.
  awi H8. am. am. am. cp(related_induced_order1 H5). split. am. au.
  nin H3. assert (forall x, inc x X -> glt r x (V x y)). ir.
  awi H3. ee. bwi H5. rwi H5 H6. cp (H6 _ H4). bwi H7. ufi T H7.
  Ztac. am. am. gprops.
  nin H2. awi H3. ee. assert (forall x, inc x X -> inc (V x y) X).
  ir. bwi H5. rwi H5 H6. cp (H6 _ H7). ufi T H8. bwi H8. Ztac. am. am.
  cp (integer_induction_stable H2 H7).
  cp (induction_defined_pr (fun n : Set => V n y) y0). simpl in H9. ee.
  set (f:= induction_defined (fun n : Set => V n y) y0) in *.
  assert (forall n, inc n Bnat -> glt r (W n f) (W (succ n) f)).
  ir. rw H12. aw. app H4. app H8. app inc_W_target. nin H10; am. rww H9. am.
  assert (forall n, inc n Bnat -> gle r (W n f) (W (succ n) f)).
  ir. cp (H13 _ H14). nin H15. am. assert (sub (target f) (substrate r)).
  ap (sub_trans H8 H1). nin H10.
  cp (increasing_prop H H10 H9 H15 H14). cp (H0 _ H17). nin H18.
  ee. nin H20. ee. assert (inc (succ x) Bnat). fprops.
  assert (cardinal_le x (succ x)). app is_less_than_succ. fprops.
  cp (H21 _ H22 H23). cp (H13 _ H20). nin H25. elim H26. uf W. sy; am.
  gprops.
Qed.

Theorem decreasing_stationary: forall r, total_order r ->
  (worder r) =
  (forall f, decreasing_sequence f r -> stationary_sequence f).
Proof. ir. app iff_eq. ir. nin H0.
  red in H1. ee. assert (Ha: is_graph f). nin H1;am.
  assert (nonempty (range f)). exists (V card_zero f). aw. exists card_zero.
  app fdomain_pr1. rw H3. fprops. nin (H2 _ H4 H6). nin H7. ee.
  assert (substrate (induced_order r (range f)) = range f). aw. rwi H9 H7.
  rwi H9 H8. awi H7. nin H7. assert (inc x0 Bnat). wr H3. aw. exists x. am.
  red. ee. am. am. exists x0. split. am. ir.
  cp (H5 _ _ H10 H11 H12). cp (pr2_V H1 H7). awi H14. rwi H14 H8.
  assert (inc (V n f) (range f)). aw. exists n. app fdomain_pr1. rww H3.
  cp (H8 _ H15). awi H16. order_tac.
  aw. exists x0. app fdomain_pr1. rww H3. am. am. ir.
  red. ee. red in H; ee; am. ir.
  set (r':= opposite_order r). cp (total_order_lattice (total_order_sub H H1)).
  nin H. clear H4.
  assert (substrate r = substrate r'). uf r'. aw.
  assert (forall f : Set, increasing_sequence f r' -> stationary_sequence f).
  ir. app H0. red in H5. ee. red. ee. am. am. rww H4.
  ir. cp (H8 _ _ H9 H10 H11). ufi r' H12. awi H12. am. am.
  assert (order r'). uf r'. fprops. wri (increasing_stationary H6) H5.
  nin (lattice_directed H3). wri H4 H5. nin (H5 _ H1 H2). ufi r' H9.
  assert (induced_order (opposite_order r) x =
    opposite_order (induced_order r x)). app opposite_induced.
  rwi H10 H9. rwi maximal_opposite H9. exists x0.
  app left_directed_mimimal. fprops.
Qed.

Theorem finite_increasing_stationary: forall r, order r ->
  is_finite_set (substrate r) ->
  (forall f, increasing_sequence f r -> stationary_sequence f).
Proof. intros r H H0. wr (increasing_stationary H). ir.
  app finite_set_maximal. fprops. aw. app (sub_finite_set H1 H0). aw.
Qed.

Theorem noetherian_induction: forall r F, order r ->
  (forall X, sub X (substrate r) -> nonempty X ->
    exists a, maximal_element (induced_order r X) a) ->
  sub F (substrate r) ->
  (forall a, inc a (substrate r) -> (forall x, glt r a x -> inc x F)
    -> inc a F)
  -> F = substrate r.
Proof. ir. set (c := complement (substrate r) F). nin (emptyset_dichot c).
  app extensionality. red. ir. nin (p_or_not_p (inc x F)). tv. ir.
  assert (inc x emptyset). wr H3. uf c. rw inc_complement. intuition.
  elim (emptyset_pr H6). assert (sub c (substrate r)). uf c. app sub_complement.
  nin (H0 _ H4 H3). nin H5. awi H5. awi H6.
  assert (inc x (substrate r)). app H4.
  assert (forall y, glt r x y -> inc y F). ir. ex_middle.
  ir. assert (inc y c). uf c. rw inc_complement. split. nin H8.
  app (inc_arg2_substrate H8). am. cp (H6 y). awi H11. nin H8. cp (H11 H8).
  elim H12. sy; am. am. am. cp (H2 _ H7 H8). ufi c H5. rwi inc_complement H5.
  nin H5. elim H10. am. am. am.
Qed.

End InfiniteSets.
Export InfiniteSets.