proposition: Lemma Exercise6_4 E: infinite_set E -> (partitions E) \Eq (\Po E).
proof: Proof. move=> ifE. move/infinite_setP: (ifE) => ifE'. set (q:=partitions E). apply/card_eqP; apply: cleA. set (f:= Lf (fun y=> partition_relset y E) q (\Po (coarse E))). have injf: (injection f). apply: lf_injective. by move=> t tp;apply/setP_P; apply: sub_part_relsetX; move: tp =>/Zo_P []. move=> u v => /Zo_P [] /setP_P uE puE /Zo_P [] /setP_P vE pvE sp. exact: (part_relset_anti puE pvE). by move: (inj_source_smaller injf); rewrite /f; aw; rewrite (Exercise6_4a ifE). case: (emptyset_dichot E) => neE. by move/infinite_nz: (ifE'); rewrite neE cardinal_set0. move: neE => [y yE]. set (F:= E -s1 y). pose g u := doubleton u (E -s u). have yF: ~(inc y F) by move /setC1_P => []. have ig: (forall u v , sub u F -> sub v F -> g u = g v -> u = v). rewrite /g;move=> u v uF vF sg; case: (doubleton_inj sg); first by case. move=> [uc vc]. case: (yF); apply: uF; rewrite uc; apply /setC_P. by split => // yv; move: (vF _ yv). have pa: (forall u, sub u F -> nonempty u -> inc (g u) q). move=> u uF neu. have uE: (sub u E) by apply: (@sub_trans F)=> //; apply: sub_setC. rewrite /g;apply /partitionsP; split; last first. move=> a; case /set2_P;move => -> //; exists y; apply /setC_P;split;fprops. split; first by rewrite -/(_ \cup _) setU2_Cr. have dc: forall u, disjoint u (E -s u). by move => w; apply: disjoint_pr; move=> t tw; apply /setC_P; case. move=> a b; case/set2_P => p1; case /set2_P=> p2; rewrite ? p1 ?p2 /disjointVeq; fprops. right;apply: disjoint_S; apply: dc. move: (card_setC1_inf y ifE); rewrite -/F => cEF. have ipF: (infinite_set (\Po F)). by apply: infinite_powerset; apply /infinite_setP;rewrite - cEF. rewrite (card_powerset_rw cEF) (card_setC1_inf emptyset ipF). apply /eq_subset_cardP1. exists (Lf g ((\Po F -s1 emptyset)) q); saw; apply: lf_injective. by move=> t /setC1_P [] /setP_P tF te;apply: pa => //;apply /nonemptyP. by move=> u v /setC1_P [] /setP_P uf _ /setC1_P [] /setP_P vf _; apply: ig. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)