proposition: Lemma Exercise4_9a g n A (r := order_product g): order_fam g -> (allf g total_order) -> natp n -> cardinal (domain g) = n -> n <> \0c -> sub A (substrate r) -> sublattice r A -> forall B, free_subset r B -> (forall x, inc x B -> sup_irred (induced_order r A) x) -> sub B A -> cardinal B <=c n.
proof: Proof. move => ofg alg nN cdg nz asr slA B frB aiB sbA. have cn: cardinalp n by fprops. have snb: natp (csucc n) by fprops. move: (setX_torder_dlattice ofg alg) => [lg dlg]. case: (cleT_el (CS_cardinal B) cn) => // lncB. have [C CB cs]: exists2 C, sub C B & cardinal C = csucc n. have pa: cardinal(csucc n) <=c cardinal B. rewrite (card_nat snb). case: (finite_or_infinite (CS_cardinal B)). by move /NatP => fb; apply/cleSltP. by move => ib; apply: cle_fin_inf => //; apply /NatP. move: (cardinal_le_aux1 pa) => /(eq_subset_cardP (csucc n)). move/set_leP => [C CB eq]; exists C => //. by symmetry;rewrite - (card_nat snb); apply /card_eqP. have scA: sub C A by apply: sub_trans CB sbA. have aiC : forall x, inc x C -> sup_irred (induced_order r A) x. by move => x xc; exact (aiB _ (CB _ xc)). have frC: free_subset r C. by move => x y xc yc xy; move: (CB _ xc) (CB _ yc) => xb yb; apply:frB. apply: False_ind. clear frB aiB sbA lncB CB B. pose mip i x := inc x C /\ forall y, inc y C -> gle (Vg g i) (Vg y i) (Vg x i). have fsC: finite_set C by hnf; rewrite cs; apply /NatP. have pa: forall i, inc i (domain g) -> exists x, mip i x. move => i idg. set E := fun_image C (Vg^~i). move: (alg _ idg) => toi. have fse: finite_set E by apply: finite_fun_image. have ser: sub E (substrate (Vg g i)). move => t /funI_P [z zC ->]. move: (asr _ (scA _ zC)); rewrite /r (proj2(order_product_osr ofg)). move/prod_of_substratesP => [fgz dz h]. apply: h => //;ue. have [c cC]: nonempty C. case: (emptyset_dichot C) => // ec. by move: cs; rewrite ec cardinal_set0 => nez; case: (@succ_nz n). have ne: nonempty E by exists (Vg c i); apply /funI_P; ex_tac. move: (finite_subset_torder_greatest toi fse ne ser) => [x []]. move: toi => [oi oit]. rewrite (iorder_sr oi ser) => xe xge. move: xe => /funI_P [z zC zv]; exists z; split => //. rewrite - zv; move => y yC. have ye: inc (Vg y i) E by apply /funI_P;ex_tac. exact (iorder_gle1 (xge _ ye)). pose mx i := choose (fun x => mip i x). have mxp: forall i, inc i (domain g)-> mip i (mx i). move => i idg; rewrite /mx; apply: (choose_pr (pa _ idg)). have pb: forall i, inc i (domain g) -> inc (mx i) C. move => t ta; exact: (proj1 (mxp _ ta)). have [x xC xne]: exists2 x, inc x C & forall i, inc i (domain g) -> mx i <> x. set f := Lf mx (domain g) C. have ff: function f by apply: lf_function. move: (Imf_Starget ff); rewrite {2}/f; aw => s1. case: (equal_or_not (Imf f) C) => h. move: (image_smaller ff); rewrite {2}/f; aw; rewrite cdg. by rewrite h cs => /(cltNge (cltS nN)). move: (setC_ne (conj s1 h)) => [x] /setC_P [xc xp]. exists x=> // i idg mi; case: xp; apply /(Imf_P ff). by rewrite /f;aw; ex_tac; rewrite LfV//. set xbs:= C -s1 x. have sxbsC: sub xbs C by move => t /setC1_P []. have fsx: finite_set xbs by apply: (sub_finite_set sxbsC fsC). have nex: nonempty xbs. case: (emptyset_dichot xbs) => // xe. move: cs. have ->: C = singleton x. by apply: set1_pr => // t tC; ex_middle tnx; empty_tac1 t; apply /setC1_P. rewrite cardinal_set1 - succ_zero => bad; case: nz. by rewrite (csucc_inj CS0 (CS_nat nN) bad). have allc:(forall i, inc i (domain g) -> lattice (Vg g i)). move => i idg; move: (alg _ idg); apply: total_order_lattice. move: (sub_trans sxbsC (sub_trans scA asr)) => scbssr. move: (setX_lattice_finite_sup ofg allc fsx scbssr nex). set xb:= (supremum r xbs); rewrite -/r; move => [xbsr xbgr]. have sr: (prod_of_substrates g) = substrate r by rewrite (proj2 (order_product_osr _)). have xxb: gle r x xb. apply /(order_product_gleP); rewrite sr;split => //. by apply: asr; apply: scA. move => i idg; rewrite (xbgr _ idg). move: (mxp _ idg) => [sa sb]. move: (alg _ idg) => [ori tori]. suff: least_upper_bound (Vg g i) (fun_image xbs (Vg^~ i)) (Vg (mx i) i). by move => h; rewrite - (supremum_pr2 ori h); apply: sb. have sc: sub (fun_image xbs (Vg^~ i)) (substrate (Vg g i)). move => t /funI_P [z zbs ->]. move: (scbssr _ zbs); rewrite - sr; move /(prod_of_substratesP). by move => [_ _]; apply. have sd: inc (Vg (mx i) i) (fun_image xbs (Vg ^~i)). by apply/funI_P; exists (mx i)=> //; apply /setC1_P;split => //; apply: xne. apply /(lubP ori sc); split. split; first by apply: sc. by move => y /funI_P[z zbs ->]; apply: sb; apply sxbsC. by move => z [z1]; apply. have exfr: forall a, inc a xbs -> not (ocomparable r x a). move => a /setC1_P [aC ax]; case => lxa. by move: (frC _ _ xC aC lxa) => naw; case: ax. by move: (frC _ _ aC xC lxa). move: (sublattice_pr lg slA asr) => [lrA sra supa infa]. move: (sublattice_dr lg slA asr dlg) => dlA. have hx: forall a b, inc a A -> inc b A -> gle r x (sup r a b) -> gle r x a \/ gle r x b. move => a b aA bA. have auxP: forall a b, inc a A -> inc b A -> (gle (induced_order r A) a b <-> gle r a b). by move => s t sA tA; apply: iorder_gle0P. move: (Exercise4_8a lrA dlA (aiC _ xC)); rewrite -/r sra => h. move: (scA _ xC) => xA. move: (proj1 (slA _ _ aA bA)) => sA. move /(auxP _ _ xA sA). move : (h _ _ aA bA); rewrite - (supa _ _ aA bA) => ra rb. by move: (ra rb); case; [left | right ]; apply /auxP. have hx1: forall a b, inc a A -> inc b xbs -> gle r x (sup r a b) -> gle r x a. move => a b aA bb sab. move: (exfr _ bb) => nc. move: bb => /setC1_P [bC _]. by case: (hx _ _ aA (scA _ bC) sab) => // lxb; case: nc; left. have [f [bf sf tf]]: exists f, bijection_prop f (Nint n) xbs. suff: Nint n \Eq xbs => //. apply /card_eqP; rewrite (card_Nint nN). apply: (csucc_inj (CS_nat nN) (CS_cardinal _)). by rewrite - (csucc_pr2 xC) cs. have ff: function f by fct_tac. pose Ei i := Vfs f (Nint i). have Eiz: Ei \0c = emptyset. have aux: (sub emptyset (source f))by fprops. rewrite /Ei Nint_co00. by apply /set0_P =>t /(Vf_image_P ff aux) [s] /in_set0. have Eis: forall i, inc i Nat -> i <c n -> Ei (csucc i) = (Ei i) +s1 (Vf f i). move => i iN sin; rewrite /Ei. move: (NS_succ iN) => siN. move: (Nint_M iN) => sc. have sa: sub (Nint (csucc i)) (source f). rewrite sf; apply: Nint_M1 => //. by apply /cleSltP. have sb: sub (Nint i) (source f) by exact (sub_trans sc sa). set_extens t. move /(Vf_image_P ff sa) => [u us ->]; case: (equal_or_not u i) => ui; apply /setU1_P; [right; ue | left; apply /(Vf_image_P ff sb) ]. by exists u => //;move: us => /(NintsP iN) => h; apply/(NintP iN). case /setU1_P=> h; apply /(Vf_image_P ff sa). move /(Vf_image_P ff sb):h => [z z1 z2]; by exists z=> //; apply: sc. by rewrite h; exists i => //;apply: Nint_si. have zl: \0c <c n by move: nz => / (strict_pos_P1 nN). have Eio: Ei \1c = singleton (Vf f \0c). rewrite - succ_zero. rewrite (Eis _ NS0 zl) Eiz; apply: set1_pr => //; fprops. by move => z;case /setU1_P => // /in_set0. pose sei i := supremum r (Ei i). have sen: sei n = xb. rewrite /sei /Ei - sf -/(Imf _). by rewrite (surjective_pr0 (proj2 bf)) tf. have tb: forall i, inc i Nat -> i <c n -> inc (Vf f i) xbs. by move => i iN ltin; Wtac; rewrite sf; apply /NintP. have ns0 := NS0. have seo: sei \1c = Vf f \0c. rewrite /sei Eio (supremum_singleton (proj1 lg)) //. apply: scbssr; apply: tb; fprops. have sel: forall i, natp i -> i <=c n -> i <> \0c -> (sub (Ei i) xbs /\ least_upper_bound r (Ei i) (sei i)). move => i iN lein inz. have sa:sub (Nint i) (source f). rewrite sf; apply: Nint_M1 => //. have nei: nonempty (Ei i). exists (Vf f \0c); apply /(Vf_image_P ff sa). exists \0c => //; apply /NintP => //. by apply/ strict_pos_P1. have seix: sub (Ei i) xbs by rewrite -tf; apply: (fun_image_Starget1 ff). split; first by exact. move: (sub_finite_set seix fsx) => fe. apply: (supremum_pr1 (proj1 lg)). exact(finite_subset_lattice_sup lg fe nei (sub_trans seix scbssr)). have ses: forall i, inc i Nat -> i <c n -> i <> \0c -> sei (csucc i) = sup r (sei i) (Vf f i). move => i iN ltin inz; move: (Eis _ iN ltin) => h. move: (sel _ iN (proj1 ltin) inz) => [sa sb]. have se: has_supremum r (Ei i) by exists (sei i). move: (sub_trans sa scbssr) => sc. have sd: inc (Vf f i) (substrate r) by apply: scbssr; apply: tb. by move: (supremum_setU1 lg sc se sd); rewrite -h. suff: gle r x (sei \1c) by rewrite seo=> h;case:(exfr _ (tb _ NS0 zl)); left. rewrite - sen in xxb;move/cge1P: (zl); move: {-1} \1c (cleR CS1). apply: (Nat_induction4 NS1 nN xxb) => i /cge1P [_ /nesym] inz ltin. have iN:= (NS_lt_nat ltin nN). rewrite (ses _ iN ltin inz); apply: hx1 (tb _ iN ltin). move: i {ltin } iN (proj1 ltin) inz. apply: Nat_induction; first by move => _ []. move => t tN hrec stn _. have tn: t <c n by apply /cleSltP. have ftA: inc (Vf f t) A by apply/scA /sxbsC /(tb _ tN). case: (equal_or_not t \0c) => tnz. by rewrite tnz succ_zero seo - tnz. rewrite (ses _ tN tn tnz);apply (slA _ _ (hrec (proj1 tn) tnz) ftA). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)