Library sset10
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset9.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module InfiniteSets.
Definition induction_defined1 (h: fterm2) a p :=
induction_defined0 (fun n x => Yo (n <c p) (h n x) a) a.
Definition induction_defined_set s a E:=
change_target_fun (induction_defined s a) E.
Definition induction_defined_set0 h a E:=
change_target_fun (induction_defined0 h a) E.
Definition induction_defined_set1 h a p E:=
change_target_fun (induction_defined1 h a p) E.
Lemma induction_defined_pr1 h a p (f := induction_defined1 h a p):
inc p Bnat ->
[/\ source f = Bnat, surjection f,
Vf f \0c = a ,
(forall n, n <c p -> Vf f (succ n) = h n (Vf f n)) &
(forall n, inc n Bnat -> ~ (n <=c p) -> Vf f n = a)].
Proof.
move=> pB.
move: (induction_defined_pr0 (fun n x => Yo (n <c p) (h n x) a) a).
rewrite /f /induction_defined1.
set g := (induction_defined0 _ a).
move=> [pa pb pc pd]; split => //; move => n np.
by rewrite (pd _ (BS_le_int (proj1 np) pB)); Ytac0.
move => cnp.
have nnz: (n <> \0c) by dneg nz; rewrite nz; fprops.
move: (cpred_pr np nnz) => [pnB nsp].
rewrite nsp (pd _ pnB) Y_false //; apply /(card_le_succ_ltP _ pnB); ue.
Qed.
Lemma integer_induction1 h a p: inc p Bnat ->
exists! f, [/\ source f = Bnat, surjection f,
Vf f \0c = a ,
(forall n, n <c p -> Vf f (succ n) = h n (Vf f n)) &
(forall n, inc n Bnat -> ~ (n <=c p) -> Vf f n = a)].
Proof.
move=> pB; exists (induction_defined1 h a p); split.
by apply: induction_defined_pr1.
move: (induction_defined_pr1 h a pB) => [sx sjx x0 xs xl].
move => y [sy sjy y0 ys yl].
apply function_exten4=>//; first by ue.
rewrite sx; apply: cardinal_c_induction; first by ue.
move=> n nB eq.
case: (p_or_not_p (n <c p)) => np.
by rewrite (xs _ np) (ys _ np) eq.
have snp: (~ (succ n) <=c p) by move /card_le_succ_ltP; fprops.
have snB:= (BS_succ nB).
by rewrite (xl _ snB snp) (yl _ snB snp).
Qed.
Lemma integer_induction_stable E g a:
inc a E -> (forall x, inc x E -> inc (g x) E) ->
sub (target (induction_defined g a)) E.
Proof.
move=> eA agE.
move:(induction_defined_pr g a) => [sf sjf f0 fn] t tt.
move:((proj2 sjf) _ tt) => [x xsf <-]; rewrite sf in xsf.
move: x xsf;apply: cardinal_c_induction; first by ue.
by move=> n nB WE; rewrite fn //; apply: agE.
Qed.
Lemma integer_induction_stable0 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.
move=> aE ahE.
move:(induction_defined_pr0 h a) => [sf sjf f0 fn] t tt.
move:(proj2 sjf _ tt) => [x xsf <-]; rewrite sf in xsf.
move: x xsf;apply: cardinal_c_induction; first by ue.
by move=> n nB WE; rewrite fn //; apply: ahE.
Qed.
Lemma integer_induction_stable1 E h a p:
inc p Bnat ->
inc a E -> (forall n x, inc x E -> n <c p -> inc (h n x) E) ->
sub (target (induction_defined1 h a p)) E.
Proof.
move=> pB aE ahE.
move:(induction_defined_pr1 h a pB) => [sf sjf f0 fs lf] t tt.
move:(proj2 sjf _ tt) => [x xsf <-]; rewrite sf in xsf.
move: x xsf;apply: cardinal_c_induction; first by ue.
move=> n nB WE.
case:(p_or_not_p (n <c p)) => np.
by rewrite (fs _ np); apply: ahE.
rewrite lf; fprops; move /card_le_succ_ltP; fprops.
Qed.
Lemma change_target_pr f E (g:= change_target_fun f E):
function f -> sub (target f) E
-> (function_prop g (source f) E
/\ forall x, inc x (source f) -> Vf g x = Vf f x).
Proof.
move => ff stf; rewrite /g/change_target_fun; aw; split => //.
move: (sub_trans (f_range_graph ff) stf) => h.
move: (ff) => [_ pc pb].
split;aw; exact: function_pr.
move=> x xsf; rewrite /Vf; aw.
Qed.
Lemma induction_defined_pr_set E g a (f := induction_defined_set g a E):
inc a E -> (forall x, inc x E -> inc (g x) E) ->
[/\ function_prop f Bnat E, Vf f \0c = a &
forall n, inc n Bnat -> Vf f (succ n) = g (Vf f n)].
Proof.
move => aE ag; move: (integer_induction_stable aE ag) => st.
move: (induction_defined_pr g a)=> [sf [ff _] f0 fs].
move: (change_target_pr ff st); rewrite -/(induction_defined_set g a E) -/f.
rewrite sf; move => [pa pd].
split => //; first by rewrite -f0 pd //; fprops.
by move => n nb; rewrite (pd _ (BS_succ nb)) (fs _ nb) -pd.
Qed.
Lemma induction_defined_pr_set0 E h a (f := induction_defined_set0 h a E):
inc a E -> (forall n x, inc x E -> inc n Bnat -> inc (h n x) E) ->
[/\ function_prop f Bnat E, Vf f \0c = a &
forall n, inc n Bnat -> Vf f (succ n) = h n (Vf f n)].
Proof.
move=> aE ag; move: (integer_induction_stable0 aE ag) => st.
move: (induction_defined_pr0 h a)=> [sf [ff _] f0 fs].
move: (change_target_pr ff st); rewrite -/(induction_defined_set0 h a E) -/f.
rewrite sf; move => [pa pd].
split => //; first by rewrite -f0 pd //; fprops.
by move => n nb; rewrite (pd _ (BS_succ nb)) (fs _ nb) -pd.
Qed.
Lemma induction_defined_pr_set1 E h a p (f := induction_defined_set1 h a p E):
inc p Bnat ->
inc a E -> (forall n x, inc x E -> n <c p -> inc (h n x) E) ->
[/\ function_prop f Bnat E, Vf f \0c = a,
(forall n, n <c p -> Vf f (succ n) = h n (Vf f n)) &
(forall n, inc n Bnat -> ~ (n <=c p) -> Vf f n = a)].
Proof.
move=> pB aE ag; move: (integer_induction_stable1 pB aE ag) => st.
move: (induction_defined_pr1 h a pB)=> [sf [ff _] f0 fs1 fs2].
move: (change_target_pr ff st); rewrite -/(induction_defined_set1 h a E) -/f.
rewrite sf; move => [pa pd].
split => //; first by rewrite -f0 pd //; fprops.
move => n np.
have nB: inc n Bnat by Bnat_tac.
by rewrite (pd _ nB) (pd _ (BS_succ nB)) fs1.
by move => n nB np; rewrite (pd _ nB) (fs2 _ nB np).
Qed.
Lemma infinite_gt_one x: infinite_c x -> \1c <c x.
Proof.
by move=> h; apply: finite_lt_infinite => //; fprops.
Qed.
Lemma infinite_ge_two x: infinite_c x -> \2c <=c x.
Proof.
move => h; apply: finite_le_infinite => //; fprops.
Qed.
Lemma infinite_greater_countable1 E:
infinite_set E -> (cardinal Bnat) <=c (cardinal E).
Proof.
move=>iE;move;split;fprops.
rewrite (card_card CS_omega); apply/omega_P1 => //.
apply: OS_cardinal; fprops.
Qed.
Lemma infinite_greater_countable E:
infinite_set E -> exists F, sub F E /\ cardinal F = cardinal Bnat.
Proof.
move=> /infinite_greater_countable1 /eq_subset_cardP1 [F e ef].
exists F;split => //; by symmetry; apply /card_eqP.
Qed.
Lemma equipotent_N2_N: (coarse Bnat) \Eq Bnat.
Proof.
pose g2 a := (binom (succ a) \2c).
pose mi n m := n +c (g2 (n +c m)).
have g2B: forall a, inc a Bnat -> inc (g2 a) Bnat.
move => a aB; apply: BS_binom =>//; fprops.
have miB: forall n m, inc n Bnat -> inc m Bnat -> inc (mi n m) Bnat.
move=> n m nB mB; rewrite /mi; fprops.
have ha: forall n m, inc n Bnat -> inc m Bnat ->
(g2 (n +c m)) <=c (mi n m).
move=> n m nB mB; rewrite /mi; set t:= (g2 (n +c m)).
rewrite csumC; apply: (Bsum_M0le (g2B _ (BS_sum nB mB)) nB).
have hc: forall n, inc n Bnat-> g2 (succ n) = (g2 n) +c (succ n).
by move=> n nB; rewrite /g2 (binom_2plus0 (BS_succ nB)).
have hb: forall n m, inc n Bnat -> inc m Bnat ->
(mi n m) <c (g2 (succ (n +c m))).
move=> n m nB mB.
move: (BS_sum nB mB) => sB.
rewrite (hc _ sB) /mi; set t:= (g2 (n +c m)).
have aux: inc t Bnat by rewrite /t; apply: g2B; fprops.
rewrite csumC; apply: (csum_Mlelt aux (BS_succ sB)); fprops.
apply /(card_lt_succ_leP sB); apply: Bsum_M0le; fprops.
exists (Lf (fun z => (mi (P z) (Q z))) (coarse Bnat) Bnat); red;aw;split => //.
apply: lf_bijective; first by move => t /setX_P [_ pB qB]; fprops.
move=> u v /setX_P [pu puB quB] /setX_P [pv pvB qvB] sm.
suff ss: (P u) +c (Q u) = (P v) +c (Q v).
move: sm; rewrite /mi ss; set (w:= g2 ((P v) +c (Q v))).
have wB: inc w Bnat by apply: (g2B _ (BS_sum pvB qvB)).
move=> ss2; move: (csum_simplifiable_right wB puB pvB ss2) => sp.
rewrite sp in ss; apply: (pair_exten pu pv sp).
apply: (csum_simplifiable_left pvB quB qvB ss).
move: (ha _ _ puB quB)(hb _ _ puB quB)(ha _ _ pvB qvB)(hb _ _ pvB qvB).
rewrite sm; move=> r1 r2 r3 r4.
move: (card_le_ltT r1 r4)(card_le_ltT r3 r2)=> r5 r6.
have ls2: forall z, inc z Bnat -> \2c <=c (succ (succ z)).
move => z zB; rewrite - succ_one.
apply /(card_le_succ_succP CS1); fprops.
rewrite - succ_zero; apply /(card_le_succ_succP CS0); fprops.
have n2z: \2c <> \0c by apply: card2_nz.
suff gi: forall x y, inc x Bnat -> inc y Bnat ->
(g2 x) <c (g2 (succ y)) -> x <=c y.
move: (BS_sum puB quB) (BS_sum pvB qvB) => sun svn.
apply: (card_leA (gi _ _ sun svn r5)(gi _ _ svn sun r6)).
move=> x y xB yB; rewrite /g2.
move: (BS_succ xB) (BS_succ yB) (BS_succ (BS_succ yB)) => qa qb qc.
rewrite - (binom_monotone2 BS2 qa qc n2z (ls2 _ xB) (ls2 _ qb)).
by move /(card_lt_succ_leP qb)/(card_le_succ_succP (CS_Bnat xB)(CS_Bnat yB)).
move=> y yB.
have g2z: g2 \0c = \0c.
rewrite /g2 succ_zero (binom_bad BS1 BS2) //.
rewrite - succ_one; apply: (card_lt_succ BS1); fprops.
case: (equal_or_not y \0c) => yz.
move: BS0 => bz.
rewrite yz; exists (J \0c \0c); first by rewrite /coarse;fprops.
by rewrite pr1_pair pr2_pair /mi (bsum0l bz) g2z (bsum0l bz).
pose p k := inc k Bnat /\ y <c (g2 k).
have pa: forall k, p k -> inc k Bnat by move=> k [kB _].
have pb: (~ p \0c).
rewrite /p g2z; move=> [_ aux]; apply: (card_lt0 aux).
have pc: exists k, p k.
exists (succ y); rewrite /p; split;fprops.
move: (card_lt_succ yB) => ysy.
rewrite /g2 binom_2plus0; last by fprops.
move: (BS_succ yB) => syB.
have ax: (succ y) <=c (binom (succ y) \2c +c (succ y)).
rewrite csumC; apply: (Bsum_M0le syB (BS_binom syB BS2)).
move: (g2B _ yB)=> gB; fprops.
co_tac.
move:(least_int_prop1 pa pb pc) => [x [xB psx npx]].
move: (hc _ xB) => bp.
have p1: y <=c ((g2 x) +c x).
move: psx => [_];rewrite bp.
rewrite (csum_via_succ _ xB).
by move /(card_lt_succ_leP (BS_sum (g2B _ xB) xB)).
have p2: (g2 x) <=c y.
have cg2: cardinalp (g2 x) by move: (g2B _ xB); fprops.
have cy: cardinalp y by fprops.
case: (card_le_to_el cg2 cy) => h; first by exact h.
case: npx;red; split; assumption.
move: (g2B _ xB) => g2Bx.
move: (cdiff_pr p2); set n:= (y -c (g2 x)).
move=> p3;rewrite -p3 in p1.
have nB:inc n Bnat by apply: BS_diff.
move: (csum_le_simplifiable g2Bx nB xB p1) => lenx.
move: (cdiff_pr lenx); set m:= (x -c n).
move=> p4;rewrite -p4 in p3.
have mB: inc m Bnat by rewrite /m; apply: BS_diff.
exists (J n m); first by apply: setXp_i.
by rewrite /mi pr1_pair pr2_pair csumC p3.
Qed.
Theorem equipotent_inf2_inf E: infinite_c E ->
E ^c \2c = E.
Proof.
move=> ciE; move: (ciE) => [cE ioE].
have cEE:cardinal E = E by apply: card_card.
have isE:infinite_set E by red; rewrite cEE.
set (base := sub_functions E (coarse E)).
pose pr z := injection z /\ range (graph z) = coarse (source z).
have [psi [psibase prpsi ispsi]]:
exists psi, [/\ inc psi base, pr psi & infinite_set (source psi)].
move: (infinite_greater_countable isE) => [F [FE cFB]].
have [f [bf sf tf]]: (F \Eq (coarse F)).
move:cFB => /card_eqP eFB; eqsym.
eqtrans (coarse Bnat); [rewrite /coarse; fprops | eqtrans Bnat ].
apply: equipotent_N2_N.
by eqsym.
have ff: function f by fct_tac.
have pm: (sub (target f) (coarse E)) by rewrite tf; apply: setX_Slr.
move: (change_target_pr ff pm); set y := (change_target_fun _ _).
move => [[fy sy ty] yv].
exists y; rewrite /base sy sf; split => //.
by apply /sfun_set_P; split => //; rewrite sy sf.
split; last by rewrite sy sf - tf -(surjective_pr3 (proj2 bf)) corresp_g.
split => // u v; rewrite sy => uf vf.
by rewrite yv // yv //; apply: (bij_inj bf).
red; rewrite cFB;apply: infinite_Bnat.
set (odr := opp_order (extension_order E (coarse E))).
set (ind := Zo base (fun z => pr z /\ sub (graph psi) (graph z))).
move: (extension_osr E (coarse E)) => [oe se].
move: (opp_osr oe)=> [oo soo].
have so: sub ind (substrate odr) by rewrite soo se;apply: Zo_S.
move: (iorder_osr oo so) => [oi soi].
have ii: inductive (induced_order odr ind).
move => X; rewrite (iorder_sr oo so) => Xind.
move: (sub_trans Xind so) => aux1.
rewrite (iorder_trans _ Xind)/total_order; aw; move => [iot tot].
case: (emptyset_dichot X)=> neX.
exists psi; split; first by aw; apply: Zo_i =>//; fprops.
by rewrite neX; move=> u /in_set0.
move: neX => [rx rxX].
have Hla:forall i, inc i X -> function i.
by move => i /Xind /Zo_hi [[[ok _] _] _].
have Hlb:forall i, inc i X -> target i = coarse E.
by move => i /Xind /Zo_S /sfun_set_P [_ _ h].
have Hlc: forall x y, inc x X -> inc y X -> gle odr x y \/ gle odr y x.
move=> x y xX yX; case: (tot _ _ xX yX) => h;move: (iorder_gle1 h); fprops.
set si := Lg X source.
have Hd: forall i j, inc i (domain si) -> inc j (domain si) ->
agrees_on ((Vg si i) \cap (Vg si j)) i j.
rewrite /si; bw;move=> i j iX jX; bw.
split; [ apply: subsetI2l | by apply: subsetI2r |].
move=> a /setI2_P [asi asj].
by case: (Hlc _ _ iX jX)=> h; [ | symmetry ];apply: (extension_order_pr h).
have He:forall i, inc i (domain si) -> function_prop i (Vg si i) (coarse E).
rewrite /si; bw; move=> i iX; bw; split;fprops.
move: (extension_covering He Hd).
set x := common_ext _ _ _; rewrite/si; bw;move=> [[fx sx tx] agx _ etc].
have xb: inc x base.
rewrite /base; bw; apply /sfun_set_P; split => // => t; rewrite sx.
move /setUb_P; bw; move=> [y yX]; move: (Xind _ yX).
move => /Zo_S /sfun_set_P [_ pa _ ] ; bw; apply: pa.
have Hg: forall i, inc i X -> sub (graph i) (graph x).
move=> i iX; rewrite sub_function =>//; last by apply: Hla.
move: (etc _ iX); rewrite /agrees_on; bw;move=> [p1 p2 p3]; split => //.
move=> a asi; symmetry; exact: p3.
have sgp:(sub (graph psi) (graph x)).
apply: sub_trans (proj2 (Zo_hi (Xind _ rxX))) (Hg _ rxX).
have injx: injection x.
split=>//; move => u v;rewrite sx.
move => /setUb_P1 [a aX usa]/setUb_P1 [b bX vsb].
have [z [zX usz vsz]]:
(exists z, [/\ inc z X, inc u (source z) & inc v (source z)]).
by case: (Hlc _ _ aX bX);
move /igraph_pP /extension_orderP => [_ _ /extends_Ssource h];
[exists b | exists a ]; split => //; apply: h.
move: (etc _ zX); rewrite /agrees_on; bw;move => [_ _ aux].
rewrite (aux _ usz) (aux _ vsz).
by move: (Zo_hi (Xind _ zX)) => [[[_ iz] _] _]; apply: iz.
have rgx: (range (graph x) = coarse (source x)).
set_extens a.
move /(range_fP (proj1 injx)) => [b bsx aW]; move: bsx.
rewrite sx; move /setUb_P1=> [c cy bsc].
move: (etc _ cy); rewrite/agrees_on;bw;move => [_ _ aux].
rewrite (aux _ bsc) in aW.
move: (Xind _ cy) => /Zo_hi [[ic rc] _].
have: inc a (coarse (source c)).
rewrite -rc aW; Wtac; move: bsc; bw.
move /setX_P => [pa Ps Qs]; apply /setX_P.
split => //; apply /setUb_P1; ex_tac.
move => /setX_P [pa]; rewrite sx.
move /setUb_P1 => [b bX psb] /setUb_P1 [c cX qsc].
have [z [zX usz vsz]]:
(exists z, [/\ inc z X, inc (P a) (source z) & inc (Q a) (source z)]).
by case: (Hlc _ _ bX cX);
move /igraph_pP /extension_orderP => [_ _ /extends_Ssource h];
[exists c | exists b ]; split => //; apply: h.
have :inc a (coarse (source z)) by apply /setX_i.
move: (Xind _ zX) => /Zo_hi [[ic rc] _].
rewrite -rc; move /(range_fP (proj1 ic)) => [d dsz ->].
move: (etc _ zX); rewrite/agrees_on;bw;move => [_ _ aux].
rewrite -(aux _ dsz); apply /(range_fP fx); exists d => //.
rewrite sx; apply /setUb_P1; ex_tac.
have xi: (inc x ind) by apply: Zo_i.
exists x;split; first by aw.
move=> z zX; move: (Xind _ zX) => zi.
move: (zi) => /Zo_S zb.
apply /iorder_gleP => //; apply /igraph_pP /extension_orderP;split => //.
move: zb => /sfun_set_P [_ _ tz]; red; rewrite tx tz; split; fprops.
move: (Zorn_lemma oi ii) => [x].
rewrite /maximal (iorder_sr oo so); move => [xi aux].
have maxp: forall u, inc u ind -> extends u x -> u = x.
move=> u ui ue;apply: aux; apply /iorder_gleP => //.
move: (Zo_S ui) (Zo_S xi)=> ub xb.
apply /igraph_pP /extension_orderP;split => //.
clear aux ii.
move: xi => /Zo_P [] /sfun_set_P [fx ssxE txE] [[ijx rgx] sgx].
set (F := source x); set b:= cardinal F.
have binf:infinite_c b.
have ss: (sub (source psi) (source x)).
have fspi: function psi by move: prpsi=> [ip _]; fct_tac.
move: (domain_S sgx); rewrite? f_domain_graph //.
move: (sub_smaller ss); rewrite -/F -/b => p1.
by apply: (ge_infinite_infinite _ p1); apply /infinite_setP.
have bsq: (b = b *c b).
have a1: (F \Eq (coarse F)) by rewrite /F -rgx; apply: equipotent_range.
rewrite cprod2_pr1 /b; apply /card_eqP; eqtrans (F \times F).
case: (equal_or_not b E) => bE; first by rewrite -bE cpowx2 =>//.
have cb: cardinalp b by rewrite /b; fprops.
have bltE: (b <c E) by split ; [rewrite - cEE; exact: (sub_smaller ssxE) |].
have Hc: b *c \2c = b +c b by rewrite cprodC two_times_n.
have cb2b: b <=c (b *c \2c) by rewrite Hc; apply: csum_M0le.
have: (b *c \2c) <=c (b *c b).
apply: cprod_Mlele; fprops; apply: (infinite_ge_two binf).
rewrite - bsq => b2b2.
move: (card_leA cb2b b2b2); rewrite Hc => b2b {b2b2 cb2b Hc}.
have [/cardinal_le_aux1 lbEF _]: (cardinal b <c (cardinal(E -s F))).
case: (card_le_to_el (CS_cardinal (E -s F)) (CS_cardinal b)); last by done.
move /(csum_Mlele (card_leR cb)).
rewrite (card_card cb) (cardinal_setC ssxE) -b2b cEE => Eb; co_tac.
move:lbEF; move/(eq_subset_cardP b _) => [Y syc /card_eqP cY].
set (Z:= F \cup Y).
set (a1:= coarse F); set (a2 := F \times Y); set (a3 := Y \times Z).
move: (card_card cb) => ccb.
case: (infinite_dichot1 _ binf).
suff: (Y= emptyset).
move => eq; move: cY; rewrite eq cardinal_set0 ccb => ->; exact finite_0.
have dFY: disjoint F Y.
by apply: disjoint_pr; move=> u uF uy; move: (syc _ uy) => /setC_P [_].
move: (csum2_pr5 dFY).
rewrite -/Z -/b - (csum2_pr2a _ Y) - (csum2_pr2b _ Y) - cY ccb - b2b => cZ.
have aux: forall u v, cardinal u *c (cardinal v) = u *c v.
by move => u v; apply: cprod2_pr2; fprops; rewrite double_cardinal.
have ca1: cardinal (a2 \cup a3) = b.
have di: disjoint a2 a3.
apply: disjoint_pr; move => t /setX_P [_ af _] /setX_P [_ ay _].
by move: (syc _ ay) => /setC_P [_].
by rewrite (csum2_pr5 di) - (csum2_pr2b a2) - (csum2_pr2a a2)
- 2! cprod2_pr1 -aux -(aux Y) cZ - cY ccb -bsq -b2b.
have pzz: (coarse Z = (coarse F) \cup (a2 \cup a3)).
set_extens t.
move /setX_P => [pt]; case /setU2_P => r1.
by case /setU2_P => r2; [| apply: setU2_2]; apply: setU2_1 ;apply: setX_i.
move => xx; apply: setU2_2; apply: setU2_2 ;apply: setX_i => //.
case /setU2_P; first by apply: setX_Sll; apply: subsetU2l.
case /setU2_P => /setX_P [pa pb pc]; apply /setX_P;split => //;
try (by apply: setU2_1); (by apply: setU2_2).
have dzz: (disjoint (coarse F) (a2 \cup a3)).
red in dFY.
apply: disjoint_pr; move=> u /setX_P [_ pF qF];case /setU2_P.
move /setX_P => [_ _ qY]; empty_tac1 (Q u).
move /setX_P => [_ pY _]; empty_tac1 (P u).
have: (Y \Eq (a2 \cup a3)) by apply /card_eqP; rewrite - cY ca1.
move=> [x0 [bx0 sx0 tx0]].
set (g:= triple Z (coarse E) ((graph x) \cup (graph x0))).
have Hga: source g = Z by rewrite /g;aw.
have Hgb:graph g = ((graph x) \cup (graph x0)) by rewrite /g;aw.
have fx0: function x0 by fct_tac.
have Hgd: range (graph g) = coarse (source g).
move: bx0 => [_ sjx0].
rewrite Hga Hgb range_setU2 rgx pzz -tx0 -(surjective_pr3 sjx0) //.
have Hhf: target g = coarse E by rewrite /g; aw.
have Hge:domain (graph g) = (source g).
rewrite Hgb Hga domain_setU2; aw; rewrite sx0 //.
have ze: sub Z E.
by move=> t /setU2_P []; [apply: ssxE | move /syc => /setC_P []].
have fg: function g.
rewrite /g;apply: function_pr.
apply: fgraph_setU2; fprops; aw;rewrite sx0; exact dFY.
rewrite - Hgb Hgd /coarse Hga; apply: setX_Slr =>//.
by rewrite -Hgb Hge Hga.
have ig: injection g.
have aux1: forall a b c, inc (J a b) (graph x) -> inc (J c b) (graph x0) ->
False.
move=> u v w J1 J2; empty_tac1 v.
rewrite /F - rgx; ex_tac.
rewrite -tx0; apply: (p2graph_target fx0 J2).
apply: injective_pr_bis =>//; rewrite /related Hgb.
move=> u v w; case /setU2_P => h1; case /setU2_P => h2.
apply: (injective_pr3 ijx h1 h2).
case: (aux1 _ _ _ h1 h2).
case: (aux1 _ _ _ h2 h1).
move: bx0 => [ijx0 _]; apply: (injective_pr3 ijx0 h1 h2).
have sg: sub (graph x) (graph g) by rewrite Hgb;apply: subsetU2l.
have gi: inc g ind.
apply: Zo_i; first by apply /sfun_set_P; rewrite Hga; split => //.
split => //; apply: sub_trans sgx sg.
have egx: extends g x by rewrite /extends; split => //; rewrite txE Hhf; fprops.
apply /set0_P; move=> y yY; move: (syc _ yY) => /setC_P [_ yF].
by case: yF; rewrite/F - (maxp _ gi egx) Hga; apply: setU2_2.
Qed.
Lemma square_of_infinite a: infinite_c a -> a *c a = a.
Proof.
move=> ai.
have ca: (cardinalp a) by move: ai => [ca _].
by rewrite - cpowx2 //; apply: equipotent_inf2_inf.
Qed.
Lemma power_of_infinite a n: infinite_c a -> inc n Bnat ->
n <> \0c -> a ^c n = a.
Proof.
move=> ia nB nzn.
have ca: (cardinalp a) by move: ia => [ca _].
move: (square_of_infinite ia) => aux.
move:(cpred_pr nB nzn) => [qB] ->.
move: qB; set (q:= cpred n); move:q.
apply: cardinal_c_induction.
rewrite succ_zero; apply: cpowx1 =>//.
by move=> m mB; rewrite (pow_succ _ (BS_succ mB)); move=> ->.
Qed.
Lemma power_of_infinite1 a n: infinite_c a -> inc n Bnat ->
(a ^c n) <=c a.
Proof.
move=> ia nB.
case: (equal_or_not n \0c) => h.
rewrite h cpowx0; apply: (finite_le_infinite finite_one ia).
rewrite (power_of_infinite ia nB h);apply:card_leR; exact: (proj1 ia).
Qed.
Lemma finite_family_product a f: fgraph f ->
finite_set (domain f) -> infinite_c a ->
(forall i, inc i (domain f) -> (Vg f i) <=c a) ->
card_nz_fam f ->
(exists2 j, inc j (domain f) & (Vg f j) = a) ->
card_prod f = a.
Proof.
move=> fgf fsd ifa alea alnz [j0 j0d vj0].
set (g:= cst_graph (domain f) a).
have fgg: fgraph g by rewrite /g /cst_graph; fprops.
have df: domain f = domain g by rewrite /g/cst_graph; bw.
have le1:forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x).
by move=> t tdf; rewrite /g/cst_graph; bw; apply: alea.
move: (cprod_increasing df le1); rewrite/g cpow_pr2.
set (n:= cardinal (domain f)).
have nB: (inc n Bnat) by fprops.
have nz: n <> \0c by apply: cardinal_nonemptyset1; exists j0 =>//.
have->: (card_pow a (domain f) = card_pow a n).
rewrite /n;apply: cpow_pr; fprops.
rewrite (power_of_infinite ifa nB nz)=> le0.
set (j:= singleton j0).
have alc: (forall x, inc x (domain f) -> cardinalp (Vg f x)).
by move=> x xdf; move: (alea _ xdf) => [h _].
move: (alc _ j0d) => ca.
have sjd: (sub j (domain f)) by move=> t; move /set1_P => ->.
move: (cprod_increasing1 alc alnz sjd).
rewrite vj0 in ca.
rewrite /j cprod_trivial4 // vj0 (card_card ca)=> le2; co_tac.
Qed.
Lemma product2_infinite a b: b <=c a ->
infinite_c a -> b <> \0c -> a *c b = a.
Proof.
move=> leba ia nzb.
move :(leba) => [cb ca _].
have : ((a *c b) <=c (a *c a)) by apply: cprod_Mlele; fprops.
rewrite (square_of_infinite ia) => le1.
have le2: (a <=c (a *c b)) by apply: cprod_M1le.
co_tac.
Qed.
Lemma product2_infinite1 a b: b <=c a ->
infinite_c a -> (a *c b) <=c a.
Proof.
move =>leba ia; move :(leba) => [_ ca _].
case: (equal_or_not b \0c) => h.
rewrite h; rewrite cprod0r; apply: (finite_le_infinite finite_0 ia).
rewrite (product2_infinite leba ia h); fprops.
Qed.
Lemma product2_infinite2 a b: finite_c b ->
infinite_c a -> (a *c b) <=c a.
Proof.
move => fb ia; exact: (product2_infinite1 (finite_le_infinite fb ia) ia).
Qed.
Lemma product2_infinite4 a b c:
a <=c c -> b <=c c -> infinite_c c -> a *c b <=c c.
Proof.
move=> ac bc ci.
case: (card_le_to_ee (proj31 ac) (proj31 bc)) => ab.
case: (Bnat_dichot (proj31 bc)) => fc.
apply: Bnat_le_infinite => //;apply: BS_prod => //.
by apply: (BS_le_int ab fc).
move: (product2_infinite1 ab fc); rewrite cprodC => h; co_tac.
case: (Bnat_dichot (proj31 ac)) => fc.
apply: Bnat_le_infinite => //; apply: BS_prod => //.
by apply: (BS_le_int ab fc).
move: (product2_infinite1 ab fc) => h; co_tac.
Qed.
Lemma product2_infinite5 a b c:
a <c c -> b <c c -> infinite_c c -> a *c b <c c.
Proof.
move => l1 l2 ic.
move: (proj31_1 l1) (proj31_1 l2) => ca cb.
have [d [da [db dc]]]: exists d, a <=c d /\ b <=c d /\ d <c c.
case: (card_le_to_ee ca cb) => cab; [ exists b | exists a];fprops.
case: (finite_dichot (proj31_1 dc)) => fd.
move: (le_finite_finite fd da) (le_finite_finite fd db).
move /BnatP => aB /BnatP bB.
by apply: finite_lt_infinite => //; apply /BnatP; apply: BS_prod.
exact (card_le_ltT (product2_infinite4 da db fd) dc).
Qed.
Lemma infinite_pow x y: infinite_c x -> y <> \0c ->
infinite_c (x ^c y).
Proof.
move=> ix ynz; exact: (ge_infinite_infinite ix (cpow_Mle1 (proj1 ix) ynz)).
Qed.
Lemma infinite_pow2 x y: infinite_c x -> infinite_c y ->
infinite_c (x ^c y).
Proof. move=> ix iy; apply: (infinite_pow ix (infinite_nz iy)). Qed.
Lemma notbig_family_sum a f:
infinite_c a -> (cardinal (domain f)) <=c a ->
(forall i, inc i (domain f) -> (Vg f i) <=c a) ->
(card_sum f) <=c a.
Proof.
move=> ifa leda alea.
set (g:= Lg (domain f) (fun _ =>a)).
have dg : domain f = domain g by rewrite /g; bw.
have ale: forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x).
by move=> x xdf; rewrite /g; bw; apply: alea.
move: (csum_increasing dg ale).
rewrite csum_of_same.
move: (product2_infinite1 leda ifa) => r1.
have ->: a *c (domain f) = a *c (cardinal (domain f)).
symmetry;apply: cprod2_pr2 => //; apply: double_cardinal.
move => r2; co_tac.
Qed.
Lemma notbig_family_sum1 a f:
infinite_c a -> (cardinal (domain f)) <=c a ->
(forall i, inc i (domain f) -> (Vg f i) <=c a) ->
(exists2 j, inc j (domain f) & (Vg f j) = a) ->
(card_sum f) = a.
Proof.
move=> ifa leda alea [j0 j0d vj0].
have ca: (cardinalp a) by move: ifa => [ca _].
move: (notbig_family_sum ifa leda alea) => le1.
have: sub (singleton j0) (domain f) by move=> t /set1_P ->.
have: (forall x, inc x (domain f) -> cardinalp (Vg f x)).
by move=> x xdf; move: (alea _ xdf) => [ok _].
move=>p1 p2;move: (csum_increasing1 p1 p2).
rewrite csum_trivial4 // vj0 //.
rewrite (card_card ca)=> le2; co_tac.
Qed.
Lemma sum2_infinite1 a: infinite_c a -> a +c a = a.
Proof.
move=> ia.
have: (a +c a = a *c \2c) by rewrite cprodC two_times_n//.
rewrite (product2_infinite (infinite_ge_two ia) ia) //; fprops.
Qed.
Lemma sum2_infinite a b: b <=c a ->
infinite_c a -> a +c b = a.
Proof.
move=> leba ia; move :(leba) => [cb ca _].
apply: card_leA; last by apply: csum_M0le.
rewrite - {2} (sum2_infinite1 ia); apply: csum_Mlele; fprops.
Qed.
Lemma sum2_infinite2 a b c: cardinalp c -> infinite_c a ->
b <c a -> a = b +c c -> a = c.
Proof.
move => cc ica [ba nba] sv.
have cb: cardinalp b by co_tac.
case: (card_le_to_ee cb cc) => h.
case: (Bnat_dichot cc) => ic.
move: (BS_le_int h ic) => fc.
have fa: finite_c a by apply /BnatP; rewrite sv; apply: BS_sum.
case: (infinite_dichot1 fa ica).
by move: (sum2_infinite h ic); rewrite csumC sv.
case: (Bnat_dichot cb) => ib.
move: (BS_le_int h ib) => fb.
have fa: finite_c a by apply /BnatP; rewrite sv; apply: BS_sum.
case: (infinite_dichot1 fa ica).
by move: (sum2_infinite h ib); rewrite - sv => eq; case: nba.
Qed.
Lemma cardinal_setC1_inf E x:
infinite_set E -> cardinal E = cardinal (E -s1 x).
Proof.
move=> iE; case: (p_or_not_p (inc x E)) => xE; last by rewrite setC1_eq.
move:(card_succ_pr1 E x); rewrite setC1_K // => ces.
move: (CS_cardinal (E -s1 x)) => cF.
case: (finite_dichot cF).
move/(finite_succP cF); rewrite - ces=> h; case: (infinite_dichot2 h iE).
by move /infinite_cP; rewrite - ces; move=> [_ res].
Qed.
Lemma csum2_pr6_inf1 a b X: infinite_c X ->
cardinal a <=c X -> cardinal b <=c X ->
cardinal (a \cup b) <=c X.
Proof.
move => pa pb pc.
move: (csum_Mlele pb pc); rewrite (sum2_infinite1 pa) csum2_pr2a csum2_pr2b.
move: (csum2_pr6 a b) => h h';co_tac.
Qed.
Lemma csum_Mltlt a b c d : a <c b -> c <c d -> a +c c <c b +c d.
Proof.
move: a b c d.
suff: forall a b c d, b <=c d -> a <c b -> c <c d -> a +c c <c b +c d.
move => H a b c d le1 le2.
have cb: cardinalp b by co_tac.
have cd: cardinalp d by co_tac.
case: (card_le_to_ee cb cd) => le3; first by apply: H.
by rewrite (csumC a) (csumC b); apply: H.
move => a b c d lebd lt1 lt2.
have cd: cardinalp d by co_tac.
case: (finite_dichot cd).
move /BnatP => dB.
have bB: inc b Bnat by Bnat_tac.
have aB: inc a Bnat by Bnat_tac.
have cB: inc c Bnat by Bnat_tac.
apply: csum_Mlelt => //; co_tac.
move => ifd.
rewrite (csumC b) (sum2_infinite lebd ifd).
have ad: a <c d by co_tac.
suff: forall u v, u <=c v -> u <c d -> v <c d -> u +c v <c d.
move => H.
have ca: cardinalp a by co_tac.
have cc: cardinalp c by co_tac.
case: (card_le_to_ee ca cc) => le3; first by apply: H.
by rewrite (csumC a); apply: H.
move => u v le1 lt3 lt4.
have cv: cardinalp v by co_tac.
case: (finite_dichot cv).
move /BnatP => dB.
have uB: inc u Bnat by Bnat_tac.
apply: finite_lt_infinite => //; apply /BnatP; fprops.
by move => iv; rewrite csumC (sum2_infinite le1 iv).
Qed.
Lemma csum2_pr6_inf2 a b X: infinite_c X ->
cardinal a <c X -> cardinal b <c X ->
cardinal (a \cup b) <c X.
Proof.
move => pa pb pc.
move: (csum_Mltlt pb pc); rewrite (sum2_infinite1 pa) csum2_pr2a csum2_pr2b.
move: (csum2_pr6 a b) => h h'; co_tac.
Qed.
Lemma infinite_compl A B:
infinite_set B -> cardinal A <c cardinal B ->
cardinal (B -s A) = cardinal B.
Proof.
move => /infinite_setP p1 p2.
ex_middle nsc.
move: (sub_smaller (@sub_setC B A)) => h1.
move: (csum2_pr6_inf2 p1 p2 (conj h1 nsc)).
rewrite setU2Cr2; move: (sub_smaller (@subsetU2r A B)) => l1 l2; co_tac.
Qed.
Lemma infinite_union2 x y z:
infinite_c z -> cardinal x <c z -> cardinal y <c z ->
nonempty (z -s (x \cup y)).
Proof.
move => h1 h2 h3.
move: (csum2_pr6_inf2 h1 h2 h3) => h.
apply /nonemptyP => h4; move: (sub_smaller (empty_setC h4)).
rewrite (card_card (proj1 h1)) => h5; co_tac.
Qed.
Lemma csum_lt_infinite a b c: infinite_c c -> a <c c -> b <c c ->
(a +c b) <c c.
Proof.
move => hc; wlog : a b / a <=c b.
move => aux l1 l2.
case: (card_le_to_ee (proj31_1 l1) (proj31_1 l2)) => l3.
by apply: aux.
by rewrite csumC; apply: aux.
move => ab ac bc.
case: (finite_dichot (proj32 ab)).
move /BnatP => bb; apply: finite_lt_infinite => //; apply /BnatP.
apply: BS_sum => //; apply: (BS_le_int ab bb).
by move => ib; rewrite csumC (sum2_infinite ab ib).
Qed.
Lemma cdiff_infinite a b: infinite_c a -> b <c a -> a -c b = a.
Proof.
move => ica lba.
move: (cdiff_pr (proj1 lba)) => h1; symmetry in h1.
have cd: cardinalp (a -c b) by rewrite /card_diff; fprops.
by rewrite - (sum2_infinite2 cd ica lba h1).
Qed.
Lemma cdiff_increasing2_gen a b c:
cardinalp a -> cardinalp b -> cardinalp c ->
c <=c (a +c b) -> (c -c b) <=c a.
Proof.
move => ca cb cc h.
case:(card_le_to_el cc cb); first by move /cdiff_wrong=> ->; apply:czero_least.
move => bc.
case: (finite_dichot cc) => fc; last first.
rewrite (cdiff_infinite fc bc).
move: (cdiff_pr (proj1 bc)) => h1.
case: (card_le_to_el cc ca) => // ac.
move: (csum_lt_infinite fc ac bc)=> h2; co_tac.
move: (le_finite_finite fc (proj1 bc)) => fb.
have h2: (c -c b) <=c c.
by move: (sub_smaller (@sub_setC c b)); rewrite (card_card cc).
case: (finite_dichot ca) => fa.
by apply: cdiff_increasing2 => //; apply /BnatP.
apply: (card_leT h2).
by rewrite - (sum2_infinite (finite_le_infinite fb fa) fa).
Qed.
Lemma cdiff_pr1_gen a b: cardinalp a -> cardinalp b ->
(finite_c b \/ b <c a) -> (a +c b) -c b = a.
Proof.
move => ca cb h.
case: (finite_dichot ca).
move /BnatP => fa; apply: cdiff_pr1 => //; case: h; first by move /BnatP.
move => [pa _ ];apply: (BS_le_int pa fa).
move => ica.
have ba : b <c a by case: h => //; move => hh; apply: finite_lt_infinite.
by rewrite (sum2_infinite (proj1 ba) ica) cdiff_infinite.
Qed.
Lemma cdiff_pr2_gen a b: infinite_c b -> a <=c b -> (a +c b) -c b = \0c.
Proof.
move => icb ab.
by rewrite csumC (sum2_infinite) // cdiff_n_n.
Qed.
Definition countable_set E:= equipotent_to_subset E Bnat.
Definition countable_infinite E := countable_set E /\ infinite_set E.
Lemma countableP E:
countable_set E <-> (cardinal E) <=c (cardinal Bnat).
Proof.
apply (iff_trans (eq_subset_cardP E Bnat)).
apply:cardinal_le_aux2P; fprops.
Qed.
Lemma countable_finite_or_N E: countable_set E ->
finite_c (cardinal E) \/ cardinal E = cardinal Bnat.
Proof.
move /countableP => leB.
case: (finite_dichot (CS_cardinal E)); [ by left | move=> [_ nf]; right].
move: (infinite_greater_countable1 nf) => le1; co_tac.
Qed.
Lemma countable_finite_or_N_b E: countable_set E ->
finite_set E \/ equipotent E Bnat.
Proof.
by case /(countable_finite_or_N) => h; [ left | right; apply /card_eqP].
Qed.
Lemma countable_infiniteP E: countable_infinite E <-> equipotent E Bnat.
Proof.
split.
move => [];case /(countable_finite_or_N_b) =>//.
move=> h1 h2; case: (infinite_dichot2 h1 h2).
move /card_eqP => eq; split; first by apply /countableP; rewrite eq; fprops.
apply /infinite_setP; rewrite eq;apply /infinite_setP; apply infinite_Bnat.
Qed.
Theorem countable_sub E F: sub E F -> countable_set F ->
countable_set E.
Proof.
move=> /sub_smaller h1 /countableP h; apply /countableP; co_tac.
Qed.
Lemma countable_fun_image z f:
countable_set z -> countable_set (fun_image z f).
Proof.
move /countableP => h; apply /countableP.
move:(fun_image_smaller z f) => h1; co_tac.
Qed.
Theorem countable_product f:
finite_set (domain f) ->
(allf f countable_set) ->
countable_set (productb f).
Proof.
move=> fsd alc; apply /countableP.
set (g:= Lg (domain f) (fun i => cardinal (Vg f i))).
have ->:(cardinal (productb f) = card_prod g) by rewrite cprod_pr =>//.
apply: (@card_leT _ (card_prod (cst_graph (domain f) (cardinal Bnat)))).
apply: cprod_increasing.
rewrite /g; bw.
by rewrite /g; bw; move=> x xdf; bw; move: (alc _ xdf) => /countableP.
rewrite cpow_pr2 -(cpow_prb (cardinal Bnat) (domain f)).
apply:power_of_infinite1; last by apply /BnatP.
apply /infinite_setP; exact infinite_Bnat.
Qed.
Theorem countable_union f:
countable_set (domain f) ->
(allf f countable_set) ->
countable_set (unionb f).
Proof.
move=> cs alc; apply /countableP.
set d:= domain f.
apply: (@card_leT _ (card_sumb d (fun i => cardinal (Vg f i)))).
apply: csum_pr1 =>//.
set (h:= cst_graph d (cardinal Bnat)).
apply: (@card_leT _ (card_sum h)).
rewrite/h;apply: csum_increasing; fprops; bw.
move=> x xd; bw; move: (alc _ xd) => /countableP //.
rewrite csum_of_same - (cprod2_pr2b (cardinal Bnat) d).
apply: product2_infinite1 =>//.
move: cs => /countableP //.
apply /infinite_setP; apply: infinite_Bnat.
Qed.
Lemma card_bnat_not_zero: cardinal Bnat <> \0c.
Proof.
apply: infinite_nz; apply /infinite_setP;apply: infinite_Bnat.
Qed.
Theorem infinite_partition E: infinite_set E ->
exists f, [/\ partition_w_fam f E, (domain f) \Eq E &
(forall i, inc i (domain f) -> (countable_infinite (Vg f i)))].
Proof.
move=> iE; move: (infinite_greater_countable1 iE) => h1.
have iE': infinite_c (cardinal E) by apply /infinite_setP.
move: (product2_infinite h1 iE' card_bnat_not_zero).
rewrite cprod2_pr1; move /card_eqP=> [f [bf sf tf]].
move: (bf) => [injf sjf].
pose G a := (indexedr a (cardinal Bnat)).
set (g:= Lg (cardinal E) (fun a => image_by_fun f (G a))).
have ff: function f by fct_tac.
have ppa: forall i, inc i (cardinal E) -> sub (G i) (source f).
by move => i ie;rewrite sf; apply: setX_Sl; apply/sub1setP.
exists g; rewrite /g;split => //; bw; [ | fprops | ].
split => //; fprops.
apply: mutually_disjoint_prop;bw; move=> i j y inE jnE; bw.
move: (ppa _ inE)(ppa _ jnE) => pa pb.
move /(Vf_image_P ff pa) => [u u1 u2] /(Vf_image_P ff pb) [v v1 v2].
rewrite u2 in v2; move: (proj2 injf _ _ (pa _ u1) (pb _ v1) v2).
by move: u1 v1 => /setX_P [_ /set1_P <-] _ /setX_P [_ /set1_P <-] _ ->.
set_extens t.
move=> /setUb_P1 [y ycE]; move/(Vf_image_P ff (ppa _ ycE)).
by move => [u u1 ->]; rewrite -tf; Wtac; apply: (ppa _ ycE).
move => tE.
have tt: inc t (target f) by rewrite tf.
move: (proj2 sjf _ tt);move=> [x xsf jG].
move: xsf; rewrite sf; move /setX_P => [pax px qx].
apply /setUb_P1;ex_tac; apply /(Vf_image_P ff (ppa _ px)).
exists x => //; apply /setX_P; split;fprops.
move => i inE; bw.
have sd: (sub (G i) (source f)) by apply: ppa.
apply /countable_infiniteP /card_eqP.
by rewrite (cardinal_image sd injf) cardinal_indexedr double_cardinal.
Qed.
Lemma countable_inv_image f: surjection f ->
(forall y, inc y (target f) ->
countable_set (inv_image_by_fun f (singleton y))) ->
infinite_set (target f) ->
(source f) \Eq (target f).
Proof.
move => sf alc it.
have ff: function f by fct_tac.
set (pa := Lg (target f) (fun z=> (inv_image_by_fun f (singleton z)))).
have upa: (unionb pa = (source f)).
set_extens t.
by move /setUb_P1 => [y ytf] /(iim_fun_set1_P _ ff) [].
move => tsf; apply /setUb_P1; exists (Vf f t)=> //; first by Wtac.
apply (iim_fun_set1_P _ ff);split => //.
have md: (mutually_disjoint pa).
rewrite /pa;apply: mutually_disjoint_prop;bw.
move=> i j y itf jtf;bw; move /(iim_fun_set1_P _ ff) => [_ ->].
by move /(iim_fun_set1_P _ ff) => [_ <-].
move: (csum_pr pa).
rewrite /disjointU.
have: (equipotent (unionb (disjointU_fam pa)) (unionb pa)).
apply: equipotent_disjointU => //.
- rewrite /pa /disjointU_fam; split => //;fprops.
- rewrite/disjointU_fam /pa; bw.
- rewrite /disjointU_fam /pa; bw; move=> i idf; bw.
- eqsym; fprops.
- fprops.
move /card_eqP => ->; rewrite upa => aux.
apply/card_eqP.
have le2: ((cardinal (target f)) <=c (cardinal (source f))).
apply: surjective_cardinal_le; exists f; split => //.
apply: (card_leA _ le2).
set (cf:= Lg (domain pa) (fun a => cardinal (Vg a pa))).
set (g:= Lg (domain pa) (fun _:Set => cardinal Bnat)).
have : (cardinal (source f)) <=c (card_sum g).
rewrite aux /cf /g /pa;apply: csum_increasing; bw.
move => x xa; bw; apply /countableP; apply: alc =>//.
rewrite csum_of_same.
have -> //:((cardinal Bnat) *c (domain pa) = cardinal (target f)).
rewrite /pa; bw;rewrite - (cprod2_pr2b _ (target f)).
set (u:= cardinal (target f)).
rewrite cprodC; apply: product2_infinite.
apply: infinite_greater_countable1 =>//.
split; first (by apply: CS_cardinal); done.
apply: card_bnat_not_zero.
Qed.
Theorem infinite_finite_subsets E: infinite_set E ->
(Zo (powerset E) finite_set) \Eq E.
Proof.
move=> inE.
have icE: infinite_c (cardinal E) by split; [apply: CS_cardinal | exact].
set bF:=Zo _ _ .
pose T n := Zo (powerset E) (fun z => cardinal z = n).
have le1: (forall n, inc n Bnat -> (cardinal (T n)) <=c (cardinal E)).
move=> n nB; rewrite /T.
have cn: (cardinal n = n) by rewrite card_card; fprops.
set (K:= Zo (functions n E) injection).
set (f:= Lf (fun z => range (graph z)) K (T n)).
have ta: lf_axiom (fun z => range (graph z)) K (T n).
move=> z /Zo_P [] /fun_set_P [fz sz tz] inz.
apply: Zo_i.
apply /setP_P;rewrite -tz => //; apply: f_range_graph => //.
by rewrite (cardinal_range inz) sz cn.
have ff: function f by apply: lf_function.
set (q:= permutations n).
set (c := cardinal q).
have fc: (finite_c c).
rewrite /c /q.
have fsn: finite_set n by rewrite /finite_set cn ; fprops.
rewrite (number_of_permutations fsn).
apply : Bnat_hi; apply: BS_factorial; ue.
have cii: (forall x, inc x (target f) ->
cardinal (inv_image_by_fun f (singleton x)) = c).
move=> x ;rewrite/f; aw; move => /Zo_P [] /setP_P xE cx.
have : (equipotent n x) by rewrite - cx; fprops.
move=> [x0 [bx0 sx0 tx0]].
set (x1:= triple n E (graph x0)).
have sx1: (source x1 = n) by rewrite /x1; aw.
have tx1: (target x1 = E) by rewrite /x1; aw.
have ix1: injection x1.
have fx0: function x0 by fct_tac.
apply: injective_pr_bis.
rewrite /x1; apply: function_pr.
fprops.
apply: (@sub_trans (target x0)).
apply: f_range_graph => //.
rewrite tx0; move: xE; aw.
aw; ue.
rewrite /x1; aw;move=> u v w p1 p2; move: bx0 => [injx0 _].
apply: (injective_pr injx0 p1 p2).
set iif := inv_image_by_fun _ _.
set (g:= Lf (fun z=> (compose x1 z)) q iif).
have ta2: (lf_axiom (fun z=> (compose x1 z)) q iif).
rewrite/q/iif; move=> z zq /=; apply /iim_fun_set1_P => //.
move: zq => /Zo_P [] /fun_set_P [fz sz tz] bz.
have cxz: (x1 \coP z) by split => //; [ fct_tac | ue].
set (t:= x1 \co z).
have fr: (function t) by rewrite /t; fct_tac.
have tk: (inc t K).
apply: Zo_i; first by apply /fun_set_P;split => //; rewrite /t; aw.
apply: inj_compose1 =>//; [ move: bz => [iz _] => // | ue].
aw; split; first by exact.
have gz: sgraph (graph z) by fprops.
have ->: (x = Vf f t).
rewrite /f/t/compose; aw; rewrite compg_range //.
have ->: (range (graph z) = n).
move: bz => [_ bz]; rewrite (surjective_pr3 bz)=> //.
rewrite /x1; aw; move: bx0 => [_ bx1]; move: (surjective_pr0 bx1).
rewrite /image_of_fun /image_by_fun sx0 tx0 //.
rewrite /f; aw.
have fg: function g by rewrite /g; apply: lf_function =>//.
apply /card_eqP;eqsym; exists g; split => //; rewrite /g; aw.
apply: lf_bijective => //.
move=> u v /Zo_P [] /fun_set_P [fu su tu] bu
/Zo_P [] /fun_set_P [fv sv tv] bv sc.
apply: function_exten; try fct_tac; try ue.
move=> w wsu.
have : (Vf (compose x1 u) w = Vf (compose x1 v) w) by ue.
have c1: composable x1 v by split => //; try fct_tac; try ue.
have c2: composable x1 u by split => //; try fct_tac; try ue.
have wsv :inc w (source v) by rewrite sv - su.
aw; move: ix1 => [fx1 ix1]; apply: ix1.
rewrite sx1 -tu; Wtac;fct_tac.
rewrite sx1 -tv; Wtac;fct_tac.
move => y /(iim_fun_set1_P _ ff) [].
rewrite /f lf_source => pa; aw => rgy.
move: pa; rewrite /f; aw; move => /Zo_P [y1 iy].
have ww: sub (range (graph y)) (range (graph x1)).
rewrite -rgy /x1; aw.
move: bx0 => [_ bx0]; rewrite (surjective_pr3 bx0) tx0; fprops.
move: y1 => /fun_set_P [fy sy ty].
rewrite -tx1 in ty; move: ww;rewrite -(exists_right_composable fy ix1 ty).
move => [h [cph ch]]; exists h => //.
have sh: (source h = n) by rewrite - sy - ch; aw.
have th: (target h = n) by move: cph => [_ _ hq]; rewrite -hq.
have ih: injection h.
split;first by fct_tac.
move => v w vsh wsh sw.
have: Vf y v = Vf y w by rewrite - ch; aw; rewrite sw.
move:iy => [_ aux]; apply: aux; [rewrite sy - sh // |rewrite sy - sh //].
have bh: bijection h.
apply: bijective_if_same_finite_c_inj => //.
rewrite sh th //.
by rewrite sh/ finite_set cn; fprops.
apply: Zo_i => //; apply /fun_set_P;split => //; fct_tac.
move: (shepherd_principle ff cii).
rewrite /f; aw; move => cK.
case: (equal_or_not n \0c) => nz.
suff: (cardinal (T \0c) = \1c).
rewrite nz; move => ->; apply: finite_le_infinite; [ fprops | exact].
suff: (T \0c = singleton emptyset) by move => ->; apply: cardinal_set1.
apply: set1_pr.
apply: Zo_i; [apply:setP_0i | apply:cardinal_set0].
move => z /Zo_P [_ aux]; rewrite (cardinal_nonemptyset aux) //.
case: (finite_dichot (CS_cardinal (T n))) => finT.
apply: finite_le_infinite =>//.
change ( (cardinal (T n)) <=c (cardinal E)).
set (K1:= cardinal (functions n E)).
have k1E: (K1 = cardinal E).
rewrite /K1; change (card_pow E n = cardinal E).
have ->: (card_pow E n = card_pow (cardinal E) n)
by apply: cpow_pr;fprops.
apply: power_of_infinite => //.
have le1: ( (cardinal K) <=c (cardinal E)).
rewrite -k1E /K1; apply: sub_smaller; rewrite /K; apply: Zo_S.
apply: (@card_leT _ (cardinal K)) => //.
rewrite cK.
have i2: (c <=c (cardinal (T n))) by apply: finite_le_infinite.
have i3: (c <> \0c).
rewrite /c/q.
have fsn: finite_set n by rewrite /finite_set cn; fprops.
rewrite (number_of_permutations fsn).
rewrite cn; apply: (factorial_nz nB).
rewrite (product2_infinite i2 finT i3); fprops.
set Fn := Lg Bnat T.
have bfu: (bF = unionb Fn).
set_extens t.
move /Zo_P => [pa pb]; apply /setUb_P1; exists (cardinal t);fprops.
apply /Zo_i => //.
move /setUb_P1 => [y yb] /Zo_P [pa pb]; apply /Zo_P;split => //.
by apply /BnatP; rewrite pb.
have: (equipotent (unionb (disjointU_fam Fn)) (unionb Fn)).
apply: equipotent_disjointU; rewrite/Fn/disjointU_fam.
split => //; fprops; bw=> i iB; bw; eqsym; fprops.
apply: mutually_disjoint_prop; rewrite /Fn; bw.
move=> i j y iB jB; bw.
by move => /indexed_P [_ _ <-] /indexed_P [_ _ <-].
apply: mutually_disjoint_prop; rewrite /Fn; bw.
by move=> i j y iB jB; bw; move => /Zo_hi <- /Zo_hi <-.
move /card_eqP; rewrite -bfu => euu.
move: (csum_pr Fn).
rewrite /disjointU euu => cbf.
apply /card_eqP; apply: card_leA; last first.
apply /eq_subset_cardP1; apply /eq_subset_ex_injP.
exists (Lf (fun x => singleton x) E bF); split => //; aw.
apply: lf_injective.
move=> x xe /=; rewrite/bF; apply: Zo_i; last by apply: set1_finite.
by apply /setP_P; apply /sub1setP.
move=> u v _ _;apply: set1_inj.
have: (card_sumb (domain Fn)(fun a => cardinal (Vg Fn a)))
<=c (card_sumb (domain Fn) (fun a : Set => cardinal E)).
apply: csum_increasing; fprops; bw; rewrite /Fn;bw; move=> x xd; bw.
apply: le1 =>//.
rewrite {2} /card_sumb csum_of_same - cbf.
have -> //: ( (cardinal E) *c (domain Fn) = cardinal E).
rewrite /Fn; bw.
rewrite - (cprod2_pr2b _ Bnat).
apply: product2_infinite => //.
apply: infinite_greater_countable1 =>//.
apply: card_bnat_not_zero.
Qed.
Lemma infinite_finite_sequence E: infinite_set E ->
(Zo (sub_functions Bnat E) (fun z=> finite_set (source z))) \Eq E.
Proof.
move=> iE.
have iE': infinite_c (cardinal E) by apply /infinite_setP.
set q:= Zo _ _.
apply /card_eqP; apply: card_leA.
move: (infinite_finite_subsets infinite_Bnat).
set Fn:=Zo _ _; move=> fse.
have qu:q = unionb (Lg Fn (fun z=> (functions z E))).
set_extens t.
move => /Zo_P [] /sfun_set_P [ft sst tt] fst.
apply /setUb_P1;exists (source t) => //.
apply: Zo_i =>//; by apply /setP_P.
apply /fun_set_P;split => //.
move => /setUb_P1 [y] /Zo_P [] /setP_P pa pb /fun_set_P [ft st tt].
apply: Zo_i; [ apply /sfun_set_P;split => //; ue | rewrite st; fprops ].
have ze: (forall z, inc z Fn ->
(cardinal (functions z E)) <=c (cardinal E)).
move=> z zFn; change ((card_pow E z) <=c (cardinal E)).
have ->: (card_pow E z = card_pow (cardinal E) (cardinal z)).
apply: cpow_pr; fprops.
apply: power_of_infinite1 =>//.
move: zFn => /Zo_P [_ pa]; fprops.
move: (csum_pr1 (Lg Fn (functions^~ E))).
rewrite -qu; bw; rewrite /card_sumb;
set (g:= (Lg Fn (fun _:Set => cardinal E))).
set f0:= (Lg Fn _ ).
have fg1: (fgraph f0) by rewrite /f0; fprops.
have fg2: (fgraph g) by rewrite /g; fprops.
have df0g: domain f0 = domain g by rewrite /f0 /g; bw.
have ale: (forall x, inc x (domain f0) -> (Vg f0 x) <=c (Vg g x)).
by rewrite /f0/g; bw; move=> x xdf; bw; apply: ze.
move: (csum_increasing df0g ale) => le1 le2.
move: (infinite_greater_countable1 iE) => le3.
move: (product2_infinite1 le3 iE').
have <-: (cardinal Fn = cardinal Bnat) by apply /card_eqP.
have ->: ((cardinal E) *c (cardinal Fn) = (cardinal E) *c Fn).
apply: cprod2_pr2; fprops; apply: double_cardinal.
rewrite csum_of_same in le1.
move: (card_leT le2 le1) => le4 le5; co_tac.
apply /eq_subset_cardP1; apply /eq_subset_ex_injP.
have aux: forall v, inc v E ->
lf_axiom (fun _ => v) (singleton \0c) E by move=> vE t //=.
exists (Lf (fun z => (Lf ((fun _:Set => z))(singleton \0c) E)) E q).
split => //;aw; apply: lf_injective.
move=> z zE; apply: Zo_i.
apply /sfun_set_P;aw;split => //; last by apply: set1_sub; fprops.
apply: lf_function =>//.
aw; apply: set1_finite.
move=> u v uE vE sv.
have zs: (inc \0c (singleton \0c)) by fprops.
move: (f_equal (Vf ^~ \0c) sv); aw; apply: aux =>//.
Qed.
Definition countable_infinite E := countable_set E /\ infinite_set E.
Lemma countableP E:
countable_set E <-> (cardinal E) <=c (cardinal Bnat).
Proof.
apply (iff_trans (eq_subset_cardP E Bnat)).
apply:cardinal_le_aux2P; fprops.
Qed.
Lemma countable_finite_or_N E: countable_set E ->
finite_c (cardinal E) \/ cardinal E = cardinal Bnat.
Proof.
move /countableP => leB.
case: (finite_dichot (CS_cardinal E)); [ by left | move=> [_ nf]; right].
move: (infinite_greater_countable1 nf) => le1; co_tac.
Qed.
Lemma countable_finite_or_N_b E: countable_set E ->
finite_set E \/ equipotent E Bnat.
Proof.
by case /(countable_finite_or_N) => h; [ left | right; apply /card_eqP].
Qed.
Lemma countable_infiniteP E: countable_infinite E <-> equipotent E Bnat.
Proof.
split.
move => [];case /(countable_finite_or_N_b) =>//.
move=> h1 h2; case: (infinite_dichot2 h1 h2).
move /card_eqP => eq; split; first by apply /countableP; rewrite eq; fprops.
apply /infinite_setP; rewrite eq;apply /infinite_setP; apply infinite_Bnat.
Qed.
Theorem countable_sub E F: sub E F -> countable_set F ->
countable_set E.
Proof.
move=> /sub_smaller h1 /countableP h; apply /countableP; co_tac.
Qed.
Lemma countable_fun_image z f:
countable_set z -> countable_set (fun_image z f).
Proof.
move /countableP => h; apply /countableP.
move:(fun_image_smaller z f) => h1; co_tac.
Qed.
Theorem countable_product f:
finite_set (domain f) ->
(allf f countable_set) ->
countable_set (productb f).
Proof.
move=> fsd alc; apply /countableP.
set (g:= Lg (domain f) (fun i => cardinal (Vg f i))).
have ->:(cardinal (productb f) = card_prod g) by rewrite cprod_pr =>//.
apply: (@card_leT _ (card_prod (cst_graph (domain f) (cardinal Bnat)))).
apply: cprod_increasing.
rewrite /g; bw.
by rewrite /g; bw; move=> x xdf; bw; move: (alc _ xdf) => /countableP.
rewrite cpow_pr2 -(cpow_prb (cardinal Bnat) (domain f)).
apply:power_of_infinite1; last by apply /BnatP.
apply /infinite_setP; exact infinite_Bnat.
Qed.
Theorem countable_union f:
countable_set (domain f) ->
(allf f countable_set) ->
countable_set (unionb f).
Proof.
move=> cs alc; apply /countableP.
set d:= domain f.
apply: (@card_leT _ (card_sumb d (fun i => cardinal (Vg f i)))).
apply: csum_pr1 =>//.
set (h:= cst_graph d (cardinal Bnat)).
apply: (@card_leT _ (card_sum h)).
rewrite/h;apply: csum_increasing; fprops; bw.
move=> x xd; bw; move: (alc _ xd) => /countableP //.
rewrite csum_of_same - (cprod2_pr2b (cardinal Bnat) d).
apply: product2_infinite1 =>//.
move: cs => /countableP //.
apply /infinite_setP; apply: infinite_Bnat.
Qed.
Lemma card_bnat_not_zero: cardinal Bnat <> \0c.
Proof.
apply: infinite_nz; apply /infinite_setP;apply: infinite_Bnat.
Qed.
Theorem infinite_partition E: infinite_set E ->
exists f, [/\ partition_w_fam f E, (domain f) \Eq E &
(forall i, inc i (domain f) -> (countable_infinite (Vg f i)))].
Proof.
move=> iE; move: (infinite_greater_countable1 iE) => h1.
have iE': infinite_c (cardinal E) by apply /infinite_setP.
move: (product2_infinite h1 iE' card_bnat_not_zero).
rewrite cprod2_pr1; move /card_eqP=> [f [bf sf tf]].
move: (bf) => [injf sjf].
pose G a := (indexedr a (cardinal Bnat)).
set (g:= Lg (cardinal E) (fun a => image_by_fun f (G a))).
have ff: function f by fct_tac.
have ppa: forall i, inc i (cardinal E) -> sub (G i) (source f).
by move => i ie;rewrite sf; apply: setX_Sl; apply/sub1setP.
exists g; rewrite /g;split => //; bw; [ | fprops | ].
split => //; fprops.
apply: mutually_disjoint_prop;bw; move=> i j y inE jnE; bw.
move: (ppa _ inE)(ppa _ jnE) => pa pb.
move /(Vf_image_P ff pa) => [u u1 u2] /(Vf_image_P ff pb) [v v1 v2].
rewrite u2 in v2; move: (proj2 injf _ _ (pa _ u1) (pb _ v1) v2).
by move: u1 v1 => /setX_P [_ /set1_P <-] _ /setX_P [_ /set1_P <-] _ ->.
set_extens t.
move=> /setUb_P1 [y ycE]; move/(Vf_image_P ff (ppa _ ycE)).
by move => [u u1 ->]; rewrite -tf; Wtac; apply: (ppa _ ycE).
move => tE.
have tt: inc t (target f) by rewrite tf.
move: (proj2 sjf _ tt);move=> [x xsf jG].
move: xsf; rewrite sf; move /setX_P => [pax px qx].
apply /setUb_P1;ex_tac; apply /(Vf_image_P ff (ppa _ px)).
exists x => //; apply /setX_P; split;fprops.
move => i inE; bw.
have sd: (sub (G i) (source f)) by apply: ppa.
apply /countable_infiniteP /card_eqP.
by rewrite (cardinal_image sd injf) cardinal_indexedr double_cardinal.
Qed.
Lemma countable_inv_image f: surjection f ->
(forall y, inc y (target f) ->
countable_set (inv_image_by_fun f (singleton y))) ->
infinite_set (target f) ->
(source f) \Eq (target f).
Proof.
move => sf alc it.
have ff: function f by fct_tac.
set (pa := Lg (target f) (fun z=> (inv_image_by_fun f (singleton z)))).
have upa: (unionb pa = (source f)).
set_extens t.
by move /setUb_P1 => [y ytf] /(iim_fun_set1_P _ ff) [].
move => tsf; apply /setUb_P1; exists (Vf f t)=> //; first by Wtac.
apply (iim_fun_set1_P _ ff);split => //.
have md: (mutually_disjoint pa).
rewrite /pa;apply: mutually_disjoint_prop;bw.
move=> i j y itf jtf;bw; move /(iim_fun_set1_P _ ff) => [_ ->].
by move /(iim_fun_set1_P _ ff) => [_ <-].
move: (csum_pr pa).
rewrite /disjointU.
have: (equipotent (unionb (disjointU_fam pa)) (unionb pa)).
apply: equipotent_disjointU => //.
- rewrite /pa /disjointU_fam; split => //;fprops.
- rewrite/disjointU_fam /pa; bw.
- rewrite /disjointU_fam /pa; bw; move=> i idf; bw.
- eqsym; fprops.
- fprops.
move /card_eqP => ->; rewrite upa => aux.
apply/card_eqP.
have le2: ((cardinal (target f)) <=c (cardinal (source f))).
apply: surjective_cardinal_le; exists f; split => //.
apply: (card_leA _ le2).
set (cf:= Lg (domain pa) (fun a => cardinal (Vg a pa))).
set (g:= Lg (domain pa) (fun _:Set => cardinal Bnat)).
have : (cardinal (source f)) <=c (card_sum g).
rewrite aux /cf /g /pa;apply: csum_increasing; bw.
move => x xa; bw; apply /countableP; apply: alc =>//.
rewrite csum_of_same.
have -> //:((cardinal Bnat) *c (domain pa) = cardinal (target f)).
rewrite /pa; bw;rewrite - (cprod2_pr2b _ (target f)).
set (u:= cardinal (target f)).
rewrite cprodC; apply: product2_infinite.
apply: infinite_greater_countable1 =>//.
split; first (by apply: CS_cardinal); done.
apply: card_bnat_not_zero.
Qed.
Theorem infinite_finite_subsets E: infinite_set E ->
(Zo (powerset E) finite_set) \Eq E.
Proof.
move=> inE.
have icE: infinite_c (cardinal E) by split; [apply: CS_cardinal | exact].
set bF:=Zo _ _ .
pose T n := Zo (powerset E) (fun z => cardinal z = n).
have le1: (forall n, inc n Bnat -> (cardinal (T n)) <=c (cardinal E)).
move=> n nB; rewrite /T.
have cn: (cardinal n = n) by rewrite card_card; fprops.
set (K:= Zo (functions n E) injection).
set (f:= Lf (fun z => range (graph z)) K (T n)).
have ta: lf_axiom (fun z => range (graph z)) K (T n).
move=> z /Zo_P [] /fun_set_P [fz sz tz] inz.
apply: Zo_i.
apply /setP_P;rewrite -tz => //; apply: f_range_graph => //.
by rewrite (cardinal_range inz) sz cn.
have ff: function f by apply: lf_function.
set (q:= permutations n).
set (c := cardinal q).
have fc: (finite_c c).
rewrite /c /q.
have fsn: finite_set n by rewrite /finite_set cn ; fprops.
rewrite (number_of_permutations fsn).
apply : Bnat_hi; apply: BS_factorial; ue.
have cii: (forall x, inc x (target f) ->
cardinal (inv_image_by_fun f (singleton x)) = c).
move=> x ;rewrite/f; aw; move => /Zo_P [] /setP_P xE cx.
have : (equipotent n x) by rewrite - cx; fprops.
move=> [x0 [bx0 sx0 tx0]].
set (x1:= triple n E (graph x0)).
have sx1: (source x1 = n) by rewrite /x1; aw.
have tx1: (target x1 = E) by rewrite /x1; aw.
have ix1: injection x1.
have fx0: function x0 by fct_tac.
apply: injective_pr_bis.
rewrite /x1; apply: function_pr.
fprops.
apply: (@sub_trans (target x0)).
apply: f_range_graph => //.
rewrite tx0; move: xE; aw.
aw; ue.
rewrite /x1; aw;move=> u v w p1 p2; move: bx0 => [injx0 _].
apply: (injective_pr injx0 p1 p2).
set iif := inv_image_by_fun _ _.
set (g:= Lf (fun z=> (compose x1 z)) q iif).
have ta2: (lf_axiom (fun z=> (compose x1 z)) q iif).
rewrite/q/iif; move=> z zq /=; apply /iim_fun_set1_P => //.
move: zq => /Zo_P [] /fun_set_P [fz sz tz] bz.
have cxz: (x1 \coP z) by split => //; [ fct_tac | ue].
set (t:= x1 \co z).
have fr: (function t) by rewrite /t; fct_tac.
have tk: (inc t K).
apply: Zo_i; first by apply /fun_set_P;split => //; rewrite /t; aw.
apply: inj_compose1 =>//; [ move: bz => [iz _] => // | ue].
aw; split; first by exact.
have gz: sgraph (graph z) by fprops.
have ->: (x = Vf f t).
rewrite /f/t/compose; aw; rewrite compg_range //.
have ->: (range (graph z) = n).
move: bz => [_ bz]; rewrite (surjective_pr3 bz)=> //.
rewrite /x1; aw; move: bx0 => [_ bx1]; move: (surjective_pr0 bx1).
rewrite /image_of_fun /image_by_fun sx0 tx0 //.
rewrite /f; aw.
have fg: function g by rewrite /g; apply: lf_function =>//.
apply /card_eqP;eqsym; exists g; split => //; rewrite /g; aw.
apply: lf_bijective => //.
move=> u v /Zo_P [] /fun_set_P [fu su tu] bu
/Zo_P [] /fun_set_P [fv sv tv] bv sc.
apply: function_exten; try fct_tac; try ue.
move=> w wsu.
have : (Vf (compose x1 u) w = Vf (compose x1 v) w) by ue.
have c1: composable x1 v by split => //; try fct_tac; try ue.
have c2: composable x1 u by split => //; try fct_tac; try ue.
have wsv :inc w (source v) by rewrite sv - su.
aw; move: ix1 => [fx1 ix1]; apply: ix1.
rewrite sx1 -tu; Wtac;fct_tac.
rewrite sx1 -tv; Wtac;fct_tac.
move => y /(iim_fun_set1_P _ ff) [].
rewrite /f lf_source => pa; aw => rgy.
move: pa; rewrite /f; aw; move => /Zo_P [y1 iy].
have ww: sub (range (graph y)) (range (graph x1)).
rewrite -rgy /x1; aw.
move: bx0 => [_ bx0]; rewrite (surjective_pr3 bx0) tx0; fprops.
move: y1 => /fun_set_P [fy sy ty].
rewrite -tx1 in ty; move: ww;rewrite -(exists_right_composable fy ix1 ty).
move => [h [cph ch]]; exists h => //.
have sh: (source h = n) by rewrite - sy - ch; aw.
have th: (target h = n) by move: cph => [_ _ hq]; rewrite -hq.
have ih: injection h.
split;first by fct_tac.
move => v w vsh wsh sw.
have: Vf y v = Vf y w by rewrite - ch; aw; rewrite sw.
move:iy => [_ aux]; apply: aux; [rewrite sy - sh // |rewrite sy - sh //].
have bh: bijection h.
apply: bijective_if_same_finite_c_inj => //.
rewrite sh th //.
by rewrite sh/ finite_set cn; fprops.
apply: Zo_i => //; apply /fun_set_P;split => //; fct_tac.
move: (shepherd_principle ff cii).
rewrite /f; aw; move => cK.
case: (equal_or_not n \0c) => nz.
suff: (cardinal (T \0c) = \1c).
rewrite nz; move => ->; apply: finite_le_infinite; [ fprops | exact].
suff: (T \0c = singleton emptyset) by move => ->; apply: cardinal_set1.
apply: set1_pr.
apply: Zo_i; [apply:setP_0i | apply:cardinal_set0].
move => z /Zo_P [_ aux]; rewrite (cardinal_nonemptyset aux) //.
case: (finite_dichot (CS_cardinal (T n))) => finT.
apply: finite_le_infinite =>//.
change ( (cardinal (T n)) <=c (cardinal E)).
set (K1:= cardinal (functions n E)).
have k1E: (K1 = cardinal E).
rewrite /K1; change (card_pow E n = cardinal E).
have ->: (card_pow E n = card_pow (cardinal E) n)
by apply: cpow_pr;fprops.
apply: power_of_infinite => //.
have le1: ( (cardinal K) <=c (cardinal E)).
rewrite -k1E /K1; apply: sub_smaller; rewrite /K; apply: Zo_S.
apply: (@card_leT _ (cardinal K)) => //.
rewrite cK.
have i2: (c <=c (cardinal (T n))) by apply: finite_le_infinite.
have i3: (c <> \0c).
rewrite /c/q.
have fsn: finite_set n by rewrite /finite_set cn; fprops.
rewrite (number_of_permutations fsn).
rewrite cn; apply: (factorial_nz nB).
rewrite (product2_infinite i2 finT i3); fprops.
set Fn := Lg Bnat T.
have bfu: (bF = unionb Fn).
set_extens t.
move /Zo_P => [pa pb]; apply /setUb_P1; exists (cardinal t);fprops.
apply /Zo_i => //.
move /setUb_P1 => [y yb] /Zo_P [pa pb]; apply /Zo_P;split => //.
by apply /BnatP; rewrite pb.
have: (equipotent (unionb (disjointU_fam Fn)) (unionb Fn)).
apply: equipotent_disjointU; rewrite/Fn/disjointU_fam.
split => //; fprops; bw=> i iB; bw; eqsym; fprops.
apply: mutually_disjoint_prop; rewrite /Fn; bw.
move=> i j y iB jB; bw.
by move => /indexed_P [_ _ <-] /indexed_P [_ _ <-].
apply: mutually_disjoint_prop; rewrite /Fn; bw.
by move=> i j y iB jB; bw; move => /Zo_hi <- /Zo_hi <-.
move /card_eqP; rewrite -bfu => euu.
move: (csum_pr Fn).
rewrite /disjointU euu => cbf.
apply /card_eqP; apply: card_leA; last first.
apply /eq_subset_cardP1; apply /eq_subset_ex_injP.
exists (Lf (fun x => singleton x) E bF); split => //; aw.
apply: lf_injective.
move=> x xe /=; rewrite/bF; apply: Zo_i; last by apply: set1_finite.
by apply /setP_P; apply /sub1setP.
move=> u v _ _;apply: set1_inj.
have: (card_sumb (domain Fn)(fun a => cardinal (Vg Fn a)))
<=c (card_sumb (domain Fn) (fun a : Set => cardinal E)).
apply: csum_increasing; fprops; bw; rewrite /Fn;bw; move=> x xd; bw.
apply: le1 =>//.
rewrite {2} /card_sumb csum_of_same - cbf.
have -> //: ( (cardinal E) *c (domain Fn) = cardinal E).
rewrite /Fn; bw.
rewrite - (cprod2_pr2b _ Bnat).
apply: product2_infinite => //.
apply: infinite_greater_countable1 =>//.
apply: card_bnat_not_zero.
Qed.
Lemma infinite_finite_sequence E: infinite_set E ->
(Zo (sub_functions Bnat E) (fun z=> finite_set (source z))) \Eq E.
Proof.
move=> iE.
have iE': infinite_c (cardinal E) by apply /infinite_setP.
set q:= Zo _ _.
apply /card_eqP; apply: card_leA.
move: (infinite_finite_subsets infinite_Bnat).
set Fn:=Zo _ _; move=> fse.
have qu:q = unionb (Lg Fn (fun z=> (functions z E))).
set_extens t.
move => /Zo_P [] /sfun_set_P [ft sst tt] fst.
apply /setUb_P1;exists (source t) => //.
apply: Zo_i =>//; by apply /setP_P.
apply /fun_set_P;split => //.
move => /setUb_P1 [y] /Zo_P [] /setP_P pa pb /fun_set_P [ft st tt].
apply: Zo_i; [ apply /sfun_set_P;split => //; ue | rewrite st; fprops ].
have ze: (forall z, inc z Fn ->
(cardinal (functions z E)) <=c (cardinal E)).
move=> z zFn; change ((card_pow E z) <=c (cardinal E)).
have ->: (card_pow E z = card_pow (cardinal E) (cardinal z)).
apply: cpow_pr; fprops.
apply: power_of_infinite1 =>//.
move: zFn => /Zo_P [_ pa]; fprops.
move: (csum_pr1 (Lg Fn (functions^~ E))).
rewrite -qu; bw; rewrite /card_sumb;
set (g:= (Lg Fn (fun _:Set => cardinal E))).
set f0:= (Lg Fn _ ).
have fg1: (fgraph f0) by rewrite /f0; fprops.
have fg2: (fgraph g) by rewrite /g; fprops.
have df0g: domain f0 = domain g by rewrite /f0 /g; bw.
have ale: (forall x, inc x (domain f0) -> (Vg f0 x) <=c (Vg g x)).
by rewrite /f0/g; bw; move=> x xdf; bw; apply: ze.
move: (csum_increasing df0g ale) => le1 le2.
move: (infinite_greater_countable1 iE) => le3.
move: (product2_infinite1 le3 iE').
have <-: (cardinal Fn = cardinal Bnat) by apply /card_eqP.
have ->: ((cardinal E) *c (cardinal Fn) = (cardinal E) *c Fn).
apply: cprod2_pr2; fprops; apply: double_cardinal.
rewrite csum_of_same in le1.
move: (card_leT le2 le1) => le4 le5; co_tac.
apply /eq_subset_cardP1; apply /eq_subset_ex_injP.
have aux: forall v, inc v E ->
lf_axiom (fun _ => v) (singleton \0c) E by move=> vE t //=.
exists (Lf (fun z => (Lf ((fun _:Set => z))(singleton \0c) E)) E q).
split => //;aw; apply: lf_injective.
move=> z zE; apply: Zo_i.
apply /sfun_set_P;aw;split => //; last by apply: set1_sub; fprops.
apply: lf_function =>//.
aw; apply: set1_finite.
move=> u v uE vE sv.
have zs: (inc \0c (singleton \0c)) by fprops.
move: (f_equal (Vf ^~ \0c) sv); aw; apply: aux =>//.
Qed.
Definition stationary_sequence f :=
[/\ fgraph f, domain f = Bnat &
exists2 m, inc m Bnat & forall n, inc n Bnat -> m <=c n ->
Vg f n = Vg f m].
Definition increasing_sequence f r:=
[/\ fgraph f, domain f = Bnat, sub (range f) (substrate r) &
forall n m, inc n Bnat -> inc m Bnat -> n <=c m ->
gle r (Vg f n) (Vg f m)].
Definition decreasing_sequence f r:=
[/\ fgraph f, domain f = Bnat, sub (range f) (substrate r) &
forall n m, inc n Bnat -> inc m Bnat -> n <=c m ->
gle r (Vg f m) (Vg f n)].
Lemma increasing_seq_prop f r: order r ->
function f -> source f = Bnat -> sub (target f) (substrate r) ->
(forall n, inc n Bnat -> gle r (Vf f n) (Vf f (succ n))) ->
increasing_sequence (graph f) r.
Proof.
move => or ff sf tf ale.
split;fprops; aw.
apply: (@sub_trans (target f)) => //; apply: f_range_graph=>//.
move=> n m nB mB /cdiff_pr <-.
rewrite -/(Vf _ _ ) -/(Vf _ _).
have: (inc (m -c n) Bnat) by fprops.
move: (m -c n).
apply: cardinal_c_induction.
aw; fprops;order_tac; apply: tf; Wtac.
move=> p pB le1.
rewrite (csum_via_succ _ pB).
move: (ale _ (BS_sum nB pB))=> le2; order_tac.
Qed.
Lemma decreasing_seq_prop f r: order r ->
function f -> source f = Bnat -> sub (target f) (substrate r) ->
(forall n, inc n Bnat -> gle r (Vf f (succ n)) (Vf f n)) ->
decreasing_sequence (graph f) r.
Proof.
move => or ff sf tf ale.
split;fprops; aw.
apply: (@sub_trans (target f)) => //; apply: f_range_graph=>//.
move=> n m nB mB nm;rewrite- (cdiff_pr nm).
rewrite -/(Vf _ _ ) -/(Vf _ _).
have: (inc (m -c n) Bnat) by fprops.
move: (m -c n).
apply: cardinal_c_induction.
aw; fprops;order_tac; apply: tf; Wtac.
move=> p pB le1.
rewrite (csum_via_succ _ pB).
move: (ale _ (BS_sum nB pB)) => le2; order_tac.
Qed.
Theorem increasing_stationaryP r: order r ->
((forall X, sub X (substrate r) -> nonempty X ->
exists a, maximal (induced_order r X) a) <->
(forall f, increasing_sequence f r -> stationary_sequence f)).
Proof.
move=> or;split.
move=> hyp f [fgf df rf incf]; rewrite /stationary_sequence;split => //.
have ner: (nonempty (range f)).
exists (Vg f \0c); apply /range_gP => //.
exists \0c => //;rewrite df; fprops.
move: (hyp _ rf ner) => [a];rewrite /maximal; aw.
move => [ha]; move: (ha) => /(range_gP fgf) [x pa eq] alv; rewrite df in pa.
exists x => // => n nB xn.
move: (incf _ _ pa nB xn); rewrite -eq => h; apply: alv.
apply / iorder_gleP => //; apply /(range_gP fgf); exists n=> //; ue.
move=> h X Xsr neX.
pose T x := Zo X (fun y => glt r x y).
case: (emptyset_dichot (productb (Lg X T))) => pe.
have [x xX Tx]: (exists2 x, inc x X & T x = emptyset).
ex_middle eh.
have p1: (fgraph (Lg X T)) by fprops.
have p2: (forall i, inc i (domain (Lg X T)) -> nonempty (Vg (Lg X T) i)).
bw;move=> i iX; bw;case: (emptyset_dichot (T i))=> //ie.
case: eh; ex_tac.
by move: (setXb_ne p2); rewrite pe; move /nonemptyP.
exists x;split => //;aw=> t xt; move:(iorder_gle1 xt) => xt1.
move: (iorder_gle3 xt) => [_ tX].
ex_middle w; empty_tac1 t; apply: Zo_i =>//; split;fprops.
move:pe=> [y yp].
have p1: (forall x, inc x X -> glt r x (Vg y x)).
have aux: fgraph (Lg X T) by fprops.
move: yp => /setXb_P; bw; move => [pa pb pc] x xX.
by move: (pc _ xX); bw =>/Zo_P [].
have p2: (forall x, inc x X -> inc (Vg y x) X).
have aux: fgraph (Lg X T) by fprops.
move: yp => /setXb_P; bw; move => [pa pb pc] x xX.
by move: (pc _ xX); bw =>/Zo_P [].
move:neX => [y0 y0X].
move: (integer_induction_stable y0X p2).
move:(induction_defined_pr (Vg y) y0); simpl.
set f:= induction_defined _ _.
move=> [sf [ff _] f0 fn] tfX.
have p3: (forall n, inc n Bnat -> glt r (Vf f n) (Vf f (succ n))).
move=> n nB; rewrite fn //; apply: p1; apply: tfX; Wtac.
have p4: (forall n, inc n Bnat -> gle r (Vf f n) (Vf f (succ n))).
by move=> n nB; move: (p3 _ nB)=> [ok _].
have s2: sub (target f) (substrate r) by apply: (sub_trans tfX).
move:(h _ (increasing_seq_prop or ff sf s2 p4)) => [_ _ [m mB sm]].
have sB: (inc (succ m) Bnat) by fprops.
have lemsm: (m <=c (succ m)) by fprops.
move: (sm _ sB lemsm); move: (p3 _ mB); rewrite /Vf.
by move=> h1 h2; rewrite h2 in h1; move: h1=> [_].
Qed.
Theorem decreasing_stationaryP r: total_order r ->
((worder r) <->
(forall f, decreasing_sequence f r -> stationary_sequence f)).
Proof.
move=> tor; split => hyp.
move=> f [fgf df rf incf]; rewrite /stationary_sequence;split => //.
have ner: (nonempty (range f)).
exists (Vg f \0c); apply /range_gP => //.
exists \0c => //;rewrite df; fprops.
move: hyp=> [or wor]; move: (wor _ rf ner) => [y []]; aw.
move /(range_gP fgf) => [x xdf xv] hb.
rewrite df in xdf.
exists x => // => n nB xn.
move: (incf _ _ xdf nB xn) => pa.
have hh: inc (Vg f n) (range f)
by apply /(range_gP fgf); exists n => //; ue.
move: (iorder_gle1 (hb _ hh)); rewrite xv => leq1; order_tac.
set (r':= opp_order r).
have or: order r by move: tor => [or _].
move: (opp_osr or) => [or' sr'].
split =>//; move=>x xsr nex.
move: (total_order_lattice (total_order_sub tor xsr)) => la.
have srsr': (substrate r = substrate r') by rewrite sr'.
have aux: (forall f, increasing_sequence f r' -> stationary_sequence f).
move=> f fi; apply: hyp; move : fi => [p1 p2 p3 p4]; split => //; try ue.
move=> n m nB mB nm; move: (p4 _ _ nB mB nm); rewrite /r';bw.
by move /igraph_pP.
move: (iorder_osr or xsr) => [oi soi].
move: aux; move /(increasing_stationaryP or') => aux.
rewrite - srsr' in aux; move: (aux _ xsr nex) => [a].
rewrite /r'.
have ->: (induced_order (opp_order r) x =
opp_order (induced_order r x)) by apply: iorder_opposite.
move/(maximal_opp oi) => mi.
move: (lattice_directed la) => [_ ld].
exists a; apply: (left_directed_minimal ld mi).
Qed.
Theorem finite_increasing_stationary r: order r ->
finite_set (substrate r) ->
(forall f, increasing_sequence f r -> stationary_sequence f).
Proof.
move=> or fs; apply /(increasing_stationaryP or).
move=> X Xsr neX; move: (iorder_osr or Xsr) => [pa pb].
apply: finite_set_maximal => //; rewrite pb => //.
apply: (sub_finite_set Xsr fs).
Qed.
Theorem noetherian_induction r F: order r ->
(forall X, sub X (substrate r) -> nonempty X ->
exists a, maximal (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.
move=> or p1 p2 p3.
set (c := (substrate r) -s F).
case: (emptyset_dichot c) => ce.
apply: extensionality => //; move=> x xsr; ex_middle xsf.
empty_tac1 x; apply /setC_P;split => //.
have cs: sub c (substrate r) by rewrite /c; apply: sub_setC.
move: (p1 _ cs ce) => [a]; rewrite / maximal; aw; move => [ac am].
have aux: (forall y, glt r a y -> inc y F).
move=> y xy; ex_middle w.
have yc: (inc y c) by apply /setC_P;split => //; order_tac.
move: xy => [xy nxy]; case: nxy.
have ham: gle (induced_order r c) a y by apply /iorder_gleP.
by rewrite (am _ ham).
by move: (p3 _ (cs _ ac) aux); move: ac => /setC_P [].
Qed.
End InfiniteSets.
Export InfiniteSets.