(** * Theory of Sets EIII-3 Equipotents Sets. Cardinals Copyright INRIA (2009-2013) Apics; Marelle Team (Jose Grimm). *) (* $Id: sset7.v,v 1.147 2016/05/18 14:54:53 grimm Exp$ *) Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Export sset6. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module Bordinal. (** ** Ordinals *) (** We start with some properties of a set; [ordinal_oa] and [ordinal_o] are orderings *) Definition transitive_set E:= forall x, inc x E -> sub x E. Definition decent_set E := forall x, inc x E -> ~ (inc x x). Definition trans_dec_set E := transitive_set E /\ decent_set E. Definition asymmetric_set E := forall x y, inc x E -> inc y E -> inc x y -> inc y x -> False. Definition ordinal_oa := graph_on (fun a b => inc a b \/ a = b). Definition ordinal_o := sub_order. Definition osucc x := x +s1 x. Lemma transitive_setU x: alls x transitive_set -> transitive_set (union x). Proof. move=> alt a /setU_hi [y ay yx] t ta. move: (((alt _ yx) _ ay) _ ta) => ty; union_tac. Qed. Lemma trans_dec_setU x: alls x trans_dec_set -> trans_dec_set (union x). Proof. move=> alt; split. by apply: transitive_setU => y /alt []. by move=> a /setU_hi [y ay yx] aa; case: ((proj2 (alt _ yx)) _ ay). Qed. Lemma trans_dec_setI x: alls x trans_dec_set -> trans_dec_set (intersection x). Proof. case: (emptyset_dichot x). by move => -> _; rewrite setI_0; split => t /in_set0. move=> nea alt; split. move=> a au t ta; apply: (setI_i nea). by move=> y yx; apply: ((proj1 (alt _ yx)) _ (setI_hi au yx)). move: nea=> [y yx] a au; apply: (proj2 (alt _ yx) _ (setI_hi au yx)). Qed. Lemma succ_i x: inc x (osucc x). Proof. by apply/setU1_P; right. Qed. Hint Resolve succ_i: fprops. Lemma trans_dec_succ y: trans_dec_set y -> trans_dec_set (osucc y). Proof. move => [pa pb]; split. move => z /setU1_P; case. by move => zy t /(pa _ zy) ty; apply/setU1_P; left. by move => -> t ty; apply/setU1_P; left. by move => z zs zz; case: (pb z) => //; case /setU1_P: zs => // <-. Qed. (** Definition of an ordinal; set such sets are transitive and decent *) Definition ordinalp X:= forall Y, sub Y X -> transitive_set Y -> Y <> X -> inc Y X. Notation "f =1o g" := (forall x, ordinalp x -> f x = g x) (at level 70, format "'[hv' f '/ ' =1o g ']'", no associativity). Definition ordinal_fam g := allf g ordinalp. Definition ordinal_set E := alls E ordinalp. Lemma ordinal_trans_dec x: ordinalp x -> trans_dec_set x. Proof. move=> ox. set y := Zo (powerset x) trans_dec_set. set t := union y. have: trans_dec_set t by apply: trans_dec_setU=> z /Zo_hi. case: (equal_or_not t x); first by move=> ->. move=> ntx tct; move: (trans_dec_succ tct) => tcst. have sux: sub t x by apply: setU_s2; move =>z /Zo_P [] /setP_P. have ux:= (ox _ sux (proj1 tct) ntx). case: ((proj2 tcst) _ (succ_i t)). apply: (setU_i (succ_i t)); apply: Zo_i => //. by apply/setP_P => s /setU1_P; case; [apply: sux | move=> ->]. Qed. Lemma ordinal_transitive x: ordinalp x -> transitive_set x. Proof. by move /ordinal_trans_dec => []. Qed. Lemma ordinal_decent x: ordinalp x -> decent_set x. Proof. by move /ordinal_trans_dec => []. Qed. Lemma ordinal_irreflexive x: ordinalp x -> ~ (inc x x). Proof. by move=> ox xx; case: (ordinal_decent ox xx). Qed. (** For ordinals [inc] is the same as [strict_sub] *) Lemma ordinal_sub x y: ordinalp x -> ordinalp y -> sub x y -> x = y \/ inc x y. Proof. move=> ox oy xy; case: (equal_or_not x y); first by left. move=> nxy; right; exact: (oy _ xy (ordinal_transitive ox) nxy). Qed. Lemma ordinal_sub2 x y: ordinalp y -> inc x y -> ssub x y. Proof. move=> /ordinal_trans_dec [ty dy xy]; split; first by apply: ty. by move => ac; case: (dy _ xy); rewrite {2} ac. Qed. Lemma ordinal_sub3 x y: ordinalp y -> inc x (osucc y) -> sub x y. Proof. by move => /ordinal_transitive yb /setU1_P;case;[ apply: yb | move => ->]. Qed. Lemma ordinal_sub4P x y: ordinalp x -> ordinalp y -> (sub x y <-> inc x (osucc y)). Proof. move=> xb yb; split; last by apply: ordinal_sub3. by case /(ordinal_sub xb yb) => a; apply/setU1_P; [right | left]. Qed. (** The intersection of a set of ordinal is in the set; we deduce the trichotomy property, which says that [sub] is a total ordering for ordinals *) Lemma ordinal_setI x: nonempty x -> ordinal_set x -> inc (intersection x) x. Proof. move=> nex alo; ex_middle nux. have [pa pb]: (trans_dec_set (intersection x)). apply: trans_dec_setI =>//. by move=> y yx; move: (ordinal_trans_dec (alo _ yx)). suff: inc (intersection x) (intersection x) by move => iii; case: (pb _ iii). apply: setI_i =>// a ax; apply: (alo _ ax _ _ pa). by move=>t tix; apply: (setI_hi tix ax). by dneg xx; rewrite xx. Qed. Lemma ordinal_trichotomy x y: ordinalp x -> ordinalp y -> [\/ inc x y, inc y x | x = y]. Proof. move=> ox oy. have aux: (ordinal_set (doubleton x y)) by move=> a /set2_P [] ->. case /set2_P: (ordinal_setI (set2_ne x y) aux). move/setI2id_Pl => h;case: (ordinal_sub ox oy h) => p; in_TP4. move/setI2id_Pr => h;case: (ordinal_sub oy ox h); in_TP4. Qed. (** [X] is an ordinal if it is transitive and its elements are ordinals; or if it is the successor of an ordinal *) Lemma ordinal_pr x: transitive_set x -> ordinal_set x -> ordinalp x. Proof. move=> tx alo y sys ty nyx. move: (setC_ne (conj sys nyx)) =>[z /setC_P [zx nzy]]; move: (alo _ zx)=> oz. have zy: (sub y z). move=> t ty'; move: (alo _ (sys _ ty'))=> ot. case:(ordinal_trichotomy oz ot)=> zt //;case:nzy; [ by apply: (ty _ ty')| ue]. case: (equal_or_not y z); first by move=> ->. move=> yz; apply: (tx _ zx _ (oz _ zy ty yz)). Qed. Lemma OS_succ x: ordinalp x -> ordinalp (osucc x). Proof. move=> ox y ytx tsy yntxx. case: (equal_or_not y x) => yx; first by rewrite yx; fprops. apply/setU1_P;left; apply: ox => //. move=> t ty; move: (ytx _ ty); case /setU1_P => // tx. case: yntxx; apply: extensionality=>// s; case /setU1_P => sx. by move: (tsy _ ty); rewrite tx; apply. by rewrite sx - tx. Qed. Hint Resolve OS_succ : fprops. (** Any element of an ordinal is an ordinal, in particular, if the successor of [x] is an ordinal, so is [x]; and no set contains all ordinals *) Lemma ordinal_hi x y: ordinalp x -> inc y x -> ordinalp y. Proof. move=> ox yx. set t:= union (Zo(powerset x) (fun y=> transitive_set y /\ ordinal_set y)). have tp: ordinal_set t by move => z /setU_P [v zv /Zo_hi [_]]; apply. have ot: ordinalp t. by apply: ordinal_pr=> //;apply: transitive_setU; move=> t' /Zo_hi [pb _]. case: (ordinal_trichotomy ox ot); last by move => tx;apply: tp; ue. move=> /setU_P [v xv /Zo_P [] /setP_P aux _]. case: (ordinal_irreflexive ox (aux _ xv)). move => tx. case: (ordinal_irreflexive ot). apply: (@setU_i _ (t +s1 t)); [fprops | apply: Zo_i ]. move: (ordinal_transitive ox)=> trx. by apply/setP_P => s; case/setU1_P; [ apply: trx | move=> ->]. split; first by apply: (ordinal_transitive (OS_succ ot)). by move=> u /setU1_P; case; [ apply: tp |move=> ->// ]. Qed. Lemma ordinal_set_ordinal x: ordinalp x -> ordinal_set x. Proof. move => ox t ot; exact:(ordinal_hi ox ot). Qed. Lemma OS_succr x: ordinalp (osucc x) -> ordinalp x. Proof. move=> os ; apply: (ordinal_hi os); fprops. Qed. Definition non_coll(p: property) := ~ exists E, forall x, inc x E <-> p x. Lemma non_collP p: non_coll p <-> ~ exists E, forall x, p x -> inc x E. Proof. split => h [E Ep]; case:h; last by exists E => x /Ep. exists (Zo E p) => x; split => //; first by apply:Zo_hi. move => px; apply/Zo_P;fprops. Qed. Lemma non_collectivizing_ordinal: non_coll ordinalp. Proof. move=> [x xp]. have osx: ordinal_set x by move => t /xp. have yo: ordinalp x. by apply: ordinal_pr => // a ay b ba; move/xp: (ordinal_hi (osx _ ay) ba). by case:(ordinal_irreflexive yo); apply/xp. Qed. (** Since an ordinal is irreflexive it is asymmetric, and the successor function is injective *) Lemma ordinal_asymmetric E: ordinalp E -> asymmetric_set E. Proof. move=> oE x y xE yE xy yx. have ox:= (ordinal_hi oE xE). have xx:=(ordinal_transitive ox yx xy). case:(ordinal_irreflexive ox xx). Qed. Lemma ord_succ_inj : { when ordinalp &, injective osucc }. Proof. move=> a b oa ob eq. have /setU1_P [ab | //]: inc a (osucc b) by rewrite -eq; fprops. have /setU1_P [ba | //]: inc b (osucc a) by rewrite eq; fprops. case: (ordinal_irreflexive oa (ordinal_transitive oa ba ab)). Qed. Lemma ordo_leP x a b: gle (ordinal_o x) a b <-> [/\ inc a x, inc b x & sub a b]. Proof. apply: sub_gleP. Qed. Lemma ordo_ltP x a b: ordinalp x -> inc a x -> inc b x -> (glt (ordinal_o x) a b <-> inc a b). Proof. move=> ox ac bc. have ob:= (ordinal_hi ox bc). split. move => [/ordo_leP [_ _ sab]] nab. by case: (ordinal_sub (ordinal_hi ox ac) ob sab). by move => /(ordinal_sub2 ob) [sab nab]; split => //;apply /ordo_leP. Qed. (** If [p x] holds for some ordinal, then [p] holds for a least ordinal (for [sub]) *) Definition least_ordinal (p: property) x:= intersection (Zo (osucc x) p). Lemma least_ordinal1 x (p: property) (y:= least_ordinal p x) : ordinalp x -> p x -> [/\ ordinalp y, p y & forall z, ordinalp z -> p z -> sub y z]. Proof. move=> ox px. set (t:= Zo (osucc x) p). have xt: inc x t by apply /Zo_i; fprops. have net: nonempty t by exists x. have osbx:= (OS_succ ox). have alo: (ordinal_set t) by move => a /Zo_S /(ordinal_hi osbx). have h:= (ordinal_setI net alo). split;[by apply: alo | by move: h => /Zo_hi |]. have sxt: sub (intersection t) x by apply: setI_s1. move=> z oz pz. have aux: inc z t -> sub y z by move=> zt w wi; apply: (setI_hi wi zt). case: (ordinal_trichotomy ox oz) => ty. - exact: (sub_trans sxt (ordinal_transitive oz ty)). - by apply: aux; apply: Zo_i => //;apply/setU1_P; left. - apply: aux; ue. Qed. (** On an ordinal, [inc] and [sub] induce the same ordering, which is a well-ordering *) Lemma ordinal_same_wo x: ordinalp x -> ordinal_oa x = ordinal_o x. Proof. move=> ox. set_extens t; move/Zo_P => [pa pb]; move/setX_P: (pa) => [_ qa qb]; move:(ordinal_hi ox qa) (ordinal_hi ox qb) => ra rb; apply/Zo_i => //. - by apply: ordinal_sub3 => //; apply/setU1_P. - by apply/setU1_P; apply /ordinal_sub4P. Qed. Lemma ordinal_o_wor x: ordinalp x -> worder (ordinal_o x). Proof. move=> ox. have [pa pb]:= (sub_osr x). apply: (worder_prop_rev pa); rewrite pb => y yE nex. have p1: (ordinal_set y) by move=> a ax; move: (yE _ ax) => /(ordinal_hi ox). have hh: sub y (substrate (sub_order x)) by ue. have ix:= (ordinal_setI nex p1); ex_tac => z zy. by apply/ordo_leP;split; [apply: yE | apply: yE | apply: setI_s1 ]. Qed. Lemma ordinal_worder x: ordinalp x -> worder (ordinal_oa x). Proof. by move=> ox; rewrite ordinal_same_wo //; apply: ordinal_o_wor. Qed. (** If [x] is an element of an ordinal [E], the set of elements less than [x] (for the ordering of [E]) is [x] *) Lemma ordinal_segment1 E x: trans_dec_set E -> inc x E -> segment (ordinal_oa E) x = x. Proof. move => [tE dE] xE. suff: segment (ordinal_oa E) x = x \cap E. by move => ->; apply/setI2id_Pl; apply: tE. rewrite /segment /ordinal_oa /interval_uo graph_on_sr //; last by fprops. set_extens y. by move/Zo_hi => [ /graph_on_P1 [pa pb pc] pd]; apply: setI2_i => //;case: pc. move /setI2_P=> [yx yE]; apply:Zo_i => //;split. by apply/graph_on_P1; split => //; left. move=> xy; rewrite xy in yx; case: (dE _ xE yx). Qed. Lemma ordinal_segment E x: ordinalp E -> inc x E -> segment (ordinal_o E) x = x. Proof. move=> ox xE;rewrite -ordinal_same_wo //. apply: ordinal_segment1 => //; apply: ordinal_trans_dec =>//. Qed. (** Alternate definition of an ordinal : transitive, asymmetric and [inc] is a well-ordering *) Lemma ordinal_pr1 E: ordinalp E <-> [/\ transitive_set E, worder (ordinal_oa E) & asymmetric_set E]. Proof. split. move=> h; split => //. - by apply: ordinal_transitive. - by apply: ordinal_worder. - by apply: ordinal_asymmetric. move=> [tE woE aE] X XE tX nXE. have de: decent_set E by move=> u uE uu; case: (aE _ _ uE uE uu uu). have p0:forall b, inc b E -> inc b b \/ b = b by move=> b bE; right. have sg: (substrate (ordinal_oa E)) = E by rewrite /ordinal_oa graph_on_sr. have si: segmentp (ordinal_oa E) X. rewrite /segmentp /interval_uo /ordinal_oa sg; split => //. move=> x y xX /graph_on_P1 [yE _ h]. case: h; [ apply: (tX _ xX) | by move => -> ]. case: (well_ordered_segment woE si). by rewrite sg; move=> eXE. rewrite sg; move=> [x xs ->]; rewrite ordinal_segment1 //. Qed. Lemma ordinal_o_sr x: substrate (ordinal_o x) = x. Proof. exact: (proj2 (sub_osr _)). Qed. Lemma ordinal_o_or x: order (ordinal_o x). Proof. exact: (proj1 (sub_osr x)). Qed. Lemma ordinal_o_tor x: ordinalp x -> total_order (ordinal_o x). Proof. by move=> or; apply: (worder_total (ordinal_o_wor or)). Qed. Hint Resolve ordinal_o_or ordinal_o_wor: fprops. (** Two isomorphic ordinals are equal *) Lemma ordinal_isomorphism_unique x y f: ordinalp x -> ordinalp y -> order_isomorphism f (ordinal_o x) (ordinal_o y) -> (x = y /\ f = identity x). Proof. move=> ox oy oif. move: (oif) => [_ _ [[[ff injf] [_ surf]] srcf trgf] pf]. move: srcf trgf; rewrite !ordinal_o_sr // => srcf trgf. have Wt: forall a, inc a x -> inc (Vf f a) y. by move=> a; rewrite - srcf -trgf => asf; Wtac. have prf2:forall a b, inc a x -> inc b x -> (inc a b <-> inc (Vf f a) (Vf f b)). move=> a b ax bx. apply: (iff_trans (iff_sym (ordo_ltP ox ax bx))). rewrite - srcf in ax bx. apply: (iff_trans (order_isomorphism_siso oif ax bx)). apply /ordo_ltP => //; apply/Wt; ue. rewrite trgf srcf in surf. case: (p_or_not_p (exists2 z, inc z x & Vf f z <> z)) => H; last first. have fi: forall a, inc a x -> Vf f a = a. move=> a ax; ex_middle em; case H; ex_tac. have xy: x = y. set_extens t => tx; first by rewrite - (fi _ tx) - trgf; Wtac. by move: (surf _ tx)=> [z zx <-];rewrite (fi _ zx). split => //; apply: function_exten;aw; fprops. by rewrite xy. by move=> a; rewrite srcf;move=> ax; rewrite identity_V //; apply: fi. move:H => [z0 z0x fz0]. pose p z := inc z x /\ Vf f z <> z. move: (least_ordinal1 (p:=p) (ordinal_hi ox z0x) (conj z0x fz0)). set z := (least_ordinal p z0). move => [oz [zx pb] pc]. have p1: forall a, inc a z -> Vf f a = a. move=> a az; ex_middle aux. have ax:= (ordinal_transitive ox zx az). move: ((pc a (ordinal_hi ox ax) (conj ax aux)) _ az). by move: (ordinal_decent ox ax). case: (ordinal_trichotomy (ordinal_hi oy (Wt _ zx)) oz). + rewrite srcf in injf; move => h. by move: (injf _ _ (ordinal_transitive ox zx h) zx (p1 _ h)). + move => ww. have fzy: inc (Vf f z) y by rewrite - trgf; Wtac. move:(surf _ (ordinal_transitive oy fzy ww)) => [a ax za]. rewrite - {1} za in ww. by move /(prf2 _ _ ax zx): (ww) => /p1 h2; case pb; rewrite - za h2. + done. Qed. (** Any well-ordered set is isomorphic to an ordinal *) Lemma ordinal_isomorphism_exists r (f := ordinal_iso r): worder r -> ordinalp (target f) /\ order_isomorphism f r (ordinal_o (target f)). Proof. move=> wor;move: (proj1 wor)=> or. move: (transfinite_defined_pr target wor) => [suf sf vf]. set E:= substrate r. have fa: function f by fct_tac. have vf1: forall a b, inc a E -> (inc b (Vf f a) <-> (exists2 u, glt r u a & Vf f u = b)). move=> a b aE; rewrite (vf _ aE) /restriction_to_segment /restriction1; aw. have ssf: sub (segment r a) (source f) by rewrite sf;apply: sub_segment. split. by move/(Vf_image_P fa ssf) => [x /segmentP pa pb]; exists x. move => [x ua ub]; apply/(Vf_image_P fa ssf). by exists x => //; apply /segmentP. have incf3: forall a b, inc a (source f) -> inc b (source f) -> sub (Vf f a) (Vf f b) -> gle r a b. rewrite sf => a b aE bE sab. case: (total_order_pr2 (worder_total wor) bE aE) => // ltab. set (Bad:= Zo E (fun a => inc (Vf f a) (Vf f a))). case: (emptyset_dichot Bad)=> h. empty_tac1 b; apply /Zo_i => //. by apply: sab; apply/(vf1 _ _ aE); exists b. have BE: (sub Bad E) by rewrite /Bad; apply: Zo_S. move: (worder_prop wor BE h) => [y /Zo_P [yE iWWy] yp]. move/(vf1 _ _ yE): (iWWy) => [u us Wu]. have badu: inc u Bad by apply: Zo_i=>//; [rewrite /E;order_tac | ue ]. move: (yp _ badu) => yu; order_tac. have injf: injection f. split=>//; move=> x y xsf ysf Wxy. have p1: sub (Vf f x) (Vf f y) by rewrite Wxy; fprops. have p2: sub (Vf f y) (Vf f x) by rewrite Wxy; fprops. move: (incf3 _ _ xsf ysf p1) (incf3 _ _ ysf xsf p2) => p3 p4; order_tac. have incf: (forall a b, gle r a b -> sub (Vf f a) (Vf f b)). move=> a b ab t. have aE: (inc a E) by rewrite /E; order_tac. have bE: (inc b E) by rewrite /E; order_tac. move/(vf1 _ _ aE) =>[u us h]; apply/(vf1 _ _ bE); exists u => //; order_tac. have oi: (order_isomorphism f r (ordinal_o (target f))). split => //; [fprops | rewrite ordinal_o_sr | move=> x y xsf ysf]. split => //. split; first by move => pa; apply/ordo_leP;split => //; try Wtac; apply: incf. move/ordo_leP => [_ _ xy]; apply: (incf3 _ _ xsf ysf xy). split=>//; apply: ordinal_pr. move=> x xt y. move: ((proj2 suf) _ xt)=> [z zs <-]. rewrite sf in zs; move/ (vf1 _ _ zs) => [u us <-]. Wtac; rewrite sf; order_tac. move=> y ytf; move: ((proj2 suf) _ ytf)=> [z zs <-]. set (Bad:= Zo E (fun z => (~ (ordinalp (Vf f z))))). case: (emptyset_dichot Bad)=> h. by ex_middle h'; empty_tac1 z; apply: Zo_i =>//; rewrite/E - sf. have sBE:sub Bad E by rewrite /Bad; apply: Zo_S. move: (worder_prop wor sBE h) => [x /Zo_P [xE ioWx] xp]. case: ioWx; apply: ordinal_pr. move=> b; move/ (vf1 _ _ xE). move=> [u [ua _] Wu] t tb; move: (incf _ _ ua); apply; ue. move => a; move /(vf1 _ _ xE) => [u usr <-]. ex_middle h'. have ub:inc u Bad by apply: Zo_i => //; rewrite /E;order_tac. move: (xp _ ub) => yu; order_tac. Qed. (** [ordinal r] is the unique ordinal isomorphic to [r] *) Definition ordinal r := target (ordinal_iso r). Lemma OS_ordinal r: worder r -> ordinalp (ordinal r). Proof. move=> wor; exact: (proj1(ordinal_isomorphism_exists wor)). Qed. Lemma ordinal_o_is r: worder r -> r \Is (ordinal_o (ordinal r)). Proof. move=> wor; move:(proj2 (ordinal_isomorphism_exists wor)) => h. by exists (ordinal_iso r). Qed. Lemma ordinal_o_o x: ordinalp x -> ordinal (ordinal_o x) = x. Proof. move=> ox; move: (ordinal_o_wor ox)=> woi. have h := proj2 (ordinal_isomorphism_exists woi). by rewrite -(proj1 (ordinal_isomorphism_unique ox (OS_ordinal woi) h)). Qed. Lemma ordinal_o_isu x y: ordinalp x -> ordinalp y -> (ordinal_o x) \Is (ordinal_o y) -> x = y. Proof. move=> ox oy [f fi]; exact:proj1 (ordinal_isomorphism_unique ox oy fi). Qed. Lemma ordinal_o_isu1 r r': worder r -> worder r' -> r \Is r' -> ordinal r = ordinal r'. Proof. move=> w1 w2 or. move: (OS_ordinal w1)(OS_ordinal w2) => o1 o2. move: (ordinal_o_is w1)(ordinal_o_is w2) => i1 i2. exact: (ordinal_o_isu o1 o2 (orderIT (orderIT (orderIS i1) or) i2)). Qed. Lemma ordinal_o_isu2 r x: worder r -> ordinalp x -> r \Is (ordinal_o x) -> ordinal r = x. Proof. move=> wo ox oi. by rewrite (ordinal_o_isu1 wo (ordinal_o_wor ox) oi) (ordinal_o_o ox). Qed. Definition the_ordinal_iso r := inverse_fun (ordinal_iso r). Lemma the_ordinal_iso1 r : worder r -> order_isomorphism (the_ordinal_iso r) (ordinal_o (ordinal r)) r. Proof. move=> wor; exact(inverse_order_is (proj2 (ordinal_isomorphism_exists wor))). Qed. Lemma the_ordinal_iso2 r g: worder r -> order_isomorphism g (ordinal_o (ordinal r)) r -> g = the_ordinal_iso r. Proof. move =>wor; move: (the_ordinal_iso1 wor) => is1 is2. have ox:= (OS_ordinal wor). have wor2:=(ordinal_o_wor ox). have m1:=(order_isomorphism_w is1). have m2:=(order_isomorphism_w is2). have pc: segmentp r (substrate r) by apply: substrate_segment; fprops. have pa: segmentp r (range (graph (the_ordinal_iso r))). move: is1 => [_ _ [[_ sf] _ tf] _]. by rewrite (surjective_pr3 sf) tf. have pb: segmentp r (range (graph g)). move: is2 => [_ _ [[_ sf] _ tf] _]. by rewrite (surjective_pr3 sf) tf. exact (isomorphism_worder_unique wor2 wor pb pa m2 m1). Qed. (** We can compare two orderings; this is compatible with order isomorphism. If [E] and [E'] are two ordinals ordered by [r] and [r'], then [ordinal_leD1 E E'] says [r <= r']. In this case we have [r <= r'] iff [r] is isomorphic to a segment of [r']. We have [r < r'] iff [r] is isomorphic to [segment r' x] for some [x]. *) Definition order_le r r' := [/\ order r, order r' & exists f x, sub x (substrate r') /\ order_isomorphism f r (induced_order r' x)]. Lemma order_le_compatible r r' r1 r1': r \Is r1 -> r' \Is r1' -> (order_le r r' <-> order_le r1 r1'). Proof. move: r r' r1 r1'. suff: forall r1 r2 r3 r4, r1 \Is r3 -> r2 \Is r4 -> order_le r1 r2 -> order_le r3 r4. by move=> aux r1 r2 r3 r4 p1 p2; split;apply: aux=>//; apply: orderIS. move => r1 r2 r3 r4 /orderIS [f [o3 _ [[injf srf] sf tf] oif]]. move=> [g [_ o4 [[ig srg] sg tg] oig]]. move=> [o1 o2 [h [X [sX [_ _ [[ih srh] sh th] oih]]]]]. split => //. set Y:= Vfs g X. have sY: sub Y (substrate r4) by rewrite -tg; apply:fun_image_Starget1; fct_tac. have fg: function g by fct_tac. have ff: function f by fct_tac. have fh: function h by fct_tac. have sX': sub X (source g) by ue. have Yp1: forall x, inc x X -> inc (Vf g x) Y. move=> x xX; apply /(Vf_image_P fg sX'); ex_tac. have Yp2: forall y, inc y Y -> exists2 x, inc x X & y = Vf g x. by move=> y; move/(Vf_image_P fg sX'). move: th; aw => th. pose k x := Vf g (Vf h (Vf f x)). have ta1: forall x, inc x (substrate r3) -> inc (k x) Y. rewrite - sf /k; move=> t ts; apply: Yp1. move: (Vf_target ff ts); rewrite tf - sh => Wt; rewrite -th; Wtac. exists (Lf k (substrate r3) Y); exists Y; split => //. have aux: bijection (Lf k (substrate r3) Y). apply: lf_bijective => //. rewrite - sf; move=> u v us vs eq. move: (Vf_target ff us) (Vf_target ff vs) => Wt1 Wt2. rewrite tf - sh in Wt1 Wt2. move: (Vf_target fh Wt1)(Vf_target fh Wt2). rewrite th; aw => Wt3 Wt4. move: ig=> [_ bi];rewrite sg in bi. move: (bi _ _ (sX _ Wt3) (sX _ Wt4) eq) => eq1. move: ih=> [_ bi1];move: (bi1 _ _ Wt1 Wt2 eq1) => eq2. by apply: (proj2 injf). move=> t tY; move: (Yp2 _ tY) => [x xX ->]. rewrite - th in xX; move: ((proj2 srh) _ xX)=> [v vsf <-]. rewrite sh - tf in vsf. move: ((proj2 srf) _ vsf)=> [w wsc <-]. rewrite - sf; ex_tac. move: (iorder_osr o4 sY) => [or4 sr4]. split => //. by rewrite sr4 /bijection_prop; aw. hnf; aw; move=> u v us vs; aw. rewrite - sf in us vs; apply: (iff_trans (oif _ _ us vs)). move: (Vf_target ff us) (Vf_target ff vs); rewrite tf - sh => Wt1 Wt2. move: (Vf_target fh Wt1)(Vf_target fh Wt2); rewrite th =>Vt1 Vt2. move: (sX' _ Vt1) (sX' _ Vt2) => U1 U2; move: (Yp1 _ Vt1)(Yp1 _ Vt2) => X1 X2. apply: (iff_trans (oih _ _ Wt1 Wt2)). apply: (iff_trans(iorder_gleP r2 Vt1 Vt2)). apply: (iff_trans (oig _ _ U1 U2)); symmetry; exact: iorder_gleP. Qed. (** We say [r <= r'] if there is a order morphism; this is the same as saying that there is an isomorphism onto a subset of [r'] *) Lemma order_le_alt r r': order r -> order r' -> (exists f, order_morphism f r r') -> order_le r r'. Proof. move => or or' [f om]; split => //. move: om (order_morphism_fi om) => [oa oc [ff sf tf] isof] injf. move: (restriction_to_imageE ff); set g := restriction_to_image f => eq. have Xs: sub (target g) (substrate r'). by move => t; rewrite - tf eq/restriction1; aw; apply:fun_image_Starget. move:(iorder_osr or' Xs)=> [or1 sr1]. have bg:bijection g by apply:restriction_to_image_fb. have ss: source f = source g by rewrite eq /restriction1; aw. have aux: forall x, inc x (source g) -> Vf g x = Vf f x. move => x xsf; rewrite eq restriction1_V //; ue. exists g, (target g); split => //; split => //; first by split => //; ue. move => x y xsg ysg. apply: (iff_trans (_: gle r x y <-> (gle r' (Vf g x) (Vf g y)))). by rewrite (aux _ xsg) (aux _ ysg); apply: isof; rewrite ss. split => pa; first by apply/iorder_gleP => //; Wtac; apply: bij_function. exact: (iorder_gle1 pa). Qed. Lemma order_le_alt2 f r r' x: order r -> order r' -> sub x (substrate r') -> let F := (Lf (Vf f) (substrate r) (substrate r')) in order_isomorphism f r (induced_order r' x) -> (order_morphism F r r' /\ range (graph F) = x). Proof. move=> oa ob sxa F [ou ov' [iz sz tz] siz]. rewrite iorder_sr // in tz. have fh: function f by fct_tac. have ta1: lf_axiom (Vf f) (substrate r) (substrate r'). move=> t tu; apply: sxa; Wtac. have fF: function F by apply: lf_function. have rg: range (graph F) = x. have gF:sgraph (graph F) by fprops. rewrite - tz ;set_extens w. move/(rangeP gF) => [x0 Jg]. move: (p1graph_source fF Jg); rewrite /F; aw => xx. rewrite (Vf_pr fF Jg) /F;aw; Wtac. move=> wt;move: iz =>[_ sjh]; move: ((proj2 sjh) _ wt) => [x0 xs <-]. apply/(rangeP gF); exists x0. have ->: Vf f x0 = Vf F x0 by rewrite /F; aw; ue. apply: Vf_pr3 =>//; rewrite /F; aw; ue. split =>//;rewrite /F; split => //; first by hnf; aw. hnf; aw => x1 x2 x1s x2s; aw. rewrite - sz in x1s x2s; apply: (iff_trans (siz _ _ x1s x2s)). split; first by move/iorder_gle1. move => hh; apply/iorder_gleP => //; rewrite - tz; Wtac. Qed. Definition ordinal_leD1 r r' := [/\ ordinalp r, ordinalp r' & order_le (ordinal_o r)(ordinal_o r')]. Lemma order_le_compatible1 r r': worder r -> worder r' -> (order_le r r' <-> ordinal_leD1 (ordinal r) (ordinal r')). Proof. move=> wo1 wo2. move: (ordinal_o_is wo1)(ordinal_o_is wo2) => oi1 oi2. move: (OS_ordinal wo1)(OS_ordinal wo2) => o1 o2. rewrite (order_le_compatible oi1 oi2) /ordinal_leD1. by split => //; case. Qed. Lemma ordinal_le_P x x': ordinal_leD1 x x' <-> [/\ ordinalp x, ordinalp x' & exists f S, segmentp (ordinal_o x') S /\ order_isomorphism f (ordinal_o x) (induced_order (ordinal_o x') S)]. Proof. split. move=> [or or' [otr otr' [f [t [sx iso]]]]];split => //. move:(isomorphic_subset_segment (ordinal_o_wor or') sx) => [w [g [sw isg]]]. exists (g \co f), w; split => //. exact: (compose_order_is iso isg). move=> [or or' [f [t [[sx sxp] oi]]]];split => //; split; fprops. by exists f, t. Qed. Lemma ordinal_le_P1 x x': ordinal_leD1 x x' <-> [/\ ordinalp x, ordinalp x' & exists2 f, segmentp (ordinal_o x') (range (graph f)) & order_morphism f (ordinal_o x)(ordinal_o x')]. Proof. split; last first. move=> [or or'[f _ mf]]; split => //. move:(ordinal_o_wor or) (ordinal_o_wor or')=> [o1 _][o2 _]. by apply / (order_le_alt o1 o2); exists f. move /ordinal_le_P => [or or' [f [t [sx isof]]]]; split => //. move:(ordinal_o_wor or) (ordinal_o_wor or')=> [o1 _][o2 _]. have sxs: sub t (substrate (ordinal_o x')) by apply: sub_segment1. move: (order_le_alt2 o1 o2 sxs isof). set g := Lf _ _ _. by move => [om xp]; exists g; rewrite ? xp. Qed. Lemma ordinal_lt_P1 x x': (ordinal_leD1 x x' /\ x <> x') <-> [/\ ordinalp x, ordinalp x' & exists f y, [/\ inc y x', (range (graph f)) = segment (ordinal_o x') y & order_morphism f (ordinal_o x) (ordinal_o x')]]. Proof. split. move => [] /ordinal_le_P1 [or or' [f srf om]] nrr'. case: (well_ordered_segment (ordinal_o_wor or') srf). move=> v; case: nrr'; apply: ordinal_o_isu => //. have injf:= (order_morphism_fi om). have [o1 o2 [ff sf tf] mf] := om. exists f; split => //; split => //. split => //;apply: surjective_pr4; [fct_tac |rewrite tf v //]. move=> [t xsr rgf]. split => //; exists f, t; split => //. by rewrite - (ordinal_o_sr x'). move=> [or or' [f [t [xsr rgf om]]]]. have wodr := (ordinal_o_wor or'). move: (wodr)=> [odr _]. have p1: segmentp (ordinal_o x') (range (graph f)). by rewrite rgf;apply: segment_segment =>//; rewrite ordinal_o_sr //. split; first by apply /ordinal_le_P1 => //; split => //;exists f. move=> rr'; rewrite rr' in om. move: (unique_isomorphism_onto_segment wodr p1 om); rewrite ordinal_o_sr => idf. have xrg: inc t (segment (ordinal_o x') t). by rewrite - rgf idf /identity; aw; rewrite identity_r. apply: (not_in_segment xrg). Qed. Lemma ordinal_lt_P x x': (ordinal_leD1 x x' /\ x <> x') <-> [/\ ordinalp x, ordinalp x' & exists f y', inc y' x' /\ order_isomorphism f (ordinal_o x) (induced_order (ordinal_o x') (segment (ordinal_o x') y') )]. Proof. split; last first. move => [or or' [f [y [sx isof]]]]; apply /ordinal_lt_P1; split => //. move:(ordinal_o_wor or) (ordinal_o_wor or')=> [o1 _][o2 _]. set t := segment (ordinal_o x') y. have sxs: sub t (substrate (ordinal_o x')) by apply: sub_segment. move: (order_le_alt2 o1 o2 sxs isof). by set g := Lf _ _ _; move => [om xp]; exists g, y. move /ordinal_lt_P1. set r := (ordinal_o x); set r':= (ordinal_o x'). move=> [or or' [f [y [pa pb pc]]]]; split => //. move: pc (order_morphism_fi pc) => [oa oc [ff sf tf] isof] injf. move: (restriction_to_imageE ff) => eq. set g := restriction_to_image f. have tg : target g = segment r' y. rewrite /g eq /restriction1; aw; rewrite - pb - image_by_fun_source //. have Xs: sub (target g) (substrate r') by rewrite tg; apply: sub_segment. have [or1 sr1 ] := (iorder_osr oc Xs). have bg:bijection g by apply:restriction_to_image_fb. have ss: source f = source g by rewrite /g eq /restriction1; aw. have aux: forall x, inc x (source g) -> Vf g x = Vf f x. move => t xsf; rewrite /g eq restriction1_V //; ue. exists g, y; rewrite - tg;split => //; split => //;first by split => //; ue. move => u v xsg ysg. apply: (iff_trans (_: gle r u v <-> (gle r' (Vf g u) (Vf g v)))). by rewrite (aux _ xsg) (aux _ ysg); apply: isof; rewrite ss. split => pd; first by apply/iorder_gleP => //; Wtac; apply: bij_function. exact: (iorder_gle1 pd). Qed. Lemma ordinal_lt_pr2 a b: worder b -> (ordinal_leD1 a (ordinal b) /\ a <> (ordinal b)) -> exists f x, [/\ inc x (substrate b), (range (graph f)) = segment b x & order_morphism f (ordinal_o a) b]. Proof. move=> ob ltab; move: (ltab) =>[[oa _] _]; move: ltab. move /ordinal_lt_P1; move=> [_ op [f [x [xsp rgx om]]]]. have [g oig]: order_isomorphic (ordinal_o (ordinal b)) b. by apply: orderIS; apply: (ordinal_o_is ob). move: om (oig) => [o1 o2 [ff sf tf] pf][_ o4 [[gi gs] sg tg] pg]. have cfg: composable g f by split => //; try fct_tac; ue. rewrite ! ordinal_o_sr // in tf sf sg. have p0: function (g \co f) by fct_tac. have p3: order_morphism (g \co f) (ordinal_o a) b. split=> //; first by split;aw; rewrite ordinal_o_sr. hnf; aw; move=> u v asf bsf; aw. apply: (iff_trans (pf _ _ asf bsf)); apply/ pg; rewrite sg - tf; Wtac. set y:= (Vf g x). have p1: inc y (substrate b) by rewrite /y;Wtac; fct_tac. exists (g \co f); exists y; split => //. set_extens u. move /(range_fP p0)=> [v vsf uvW]. move: vsf; aw => vsf. have: inc (Vf f v) (segment (ordinal_o (ordinal b)) x). rewrite -rgx; Wtac. move /segmentP => xx; apply /segmentP; rewrite /y uvW; aw. by apply (order_isomorphism_sincr oig). move/segmentP=> buy. have utg: inc u (target g) by rewrite tg; order_tac. move: ((proj2 gs) _ utg) buy => [v vsg Wvg]. rewrite - sg in xsp. rewrite /y -Wvg; move/(order_isomorphism_siso oig vsg xsp) => /segmentP. rewrite -rgx; move/(range_fP ff) => [w pa pb]. apply/(range_fP p0); aw; ex_tac; rewrite pb; aw. Qed. Lemma ordinal_le_P0 x y: ordinal_leD1 x y <-> [/\ ordinalp x, ordinalp y & sub x y]. Proof. split; last first. rewrite /ordinal_leD1; move => [ox oy sxy];split => //. move: (ordinal_o_wor ox) => wox. move: (wox) => [orx _]. hnf; rewrite ordinal_o_sr //; split; fprops. exists (identity x); exists x; split => //. have ->: induced_order (ordinal_o y) x = (ordinal_o x). set_extens t. by move => /setI2_P [] /Zo_P [pa pb] pc; apply: Zo_i. move =>/ Zo_P [pa pb]; apply/setI2_P;split => //; apply: Zo_i => //. by apply: (setX_Slr sxy sxy). rewrite - {1} (ordinal_o_sr x) ; by apply: identity_is. move /ordinal_le_P => [ox oy [f [S [sS oi]]]]; split => //. move: (ordinal_o_wor oy) => woy. have [p1 p2 p3]: [/\ sub S y, ordinalp S & (induced_order (ordinal_o y) S) = ordinal_o S]. case: (well_ordered_segment woy sS). move=> Ss; rewrite {3} Ss; move: Ss; rewrite {1} ordinal_o_sr =>//. move => ->; split => //; rewrite iorder_substrate //. by move: woy => [ok _]. move=> [u]; rewrite ordinal_o_sr =>// uy. rewrite ordinal_segment //. move: (ordinal_transitive oy uy) => suy. move=> ->; split => //; first exact:(ordinal_hi oy uy). set_extens t; first by move/setI2_P => [] /Zo_P [pa pb] pc;apply /Zo_P; split. move/Zo_P =>[pa pb]; apply/setI2_i => //. by apply: Zo_i => //;apply:(setX_Sll suy). rewrite p3 in oi. by move: (ordinal_isomorphism_unique ox p2 oi)=>[-> _]. Qed. (** [ordinal_leD1 E E'] simplifies to [sub E E'] when [E] and [E'] are ordinals*) Definition ordinal_le x y := [/\ ordinalp x, ordinalp y & sub x y]. Definition ordinal_lt x y := ordinal_le x y /\ x <> y. Definition ole_on x := graph_on ordinal_le x. Notation "x <=o y" := (ordinal_le x y) (at level 60). Notation "x forall x, (x <=o a <-> inc x (osucc a)). Proof. move=> oa x; split. by move=> [pa pb pc]; apply /ordinal_sub4P. move=> aux; move: (ordinal_sub3 oa aux) => xa; split => //. apply: (ordinal_hi (OS_succ oa) aux). Qed. (** We study here [ordinal_le]; it is a well-ordering *) Lemma oltP0 x y: x [/\ ordinalp x, ordinalp y & inc x y]. Proof. split. move=> [[ox oy sxy] nxy]; split => //; case: (ordinal_sub ox oy sxy) => //. by move=> [ox oy xy]; move: (ordinal_sub2 oy xy) => [pa pb]. Qed. Lemma olt_i x y: x inc x y. Proof. by case/oltP0. Qed. Lemma oltP a: ordinalp a -> forall x, (x inc x a). Proof. move=> oa x; split; first by apply:olt_i. move => xa; apply/oltP0; split => //; exact:ordinal_hi oa xa. Qed. Lemma least_ordinal0 E (x:= intersection E): ordinal_set E -> nonempty E -> [/\ ordinalp x, inc x E & forall y, inc y E -> x <=o y]. Proof. move => sa sb. have xe:= (ordinal_setI sb sa). have ox:=(sa _ xe). split => // y yE;split;[ exact | exact (sa _ yE)| exact:(setI_s1 yE)]. Qed. Theorem wordering_ole: worder_r ordinal_le. Proof. split; first split. - move=> x y z [Kx Ky xy][_ Kz yz]. split => //; by apply: sub_trans yz. - move=> x y [Kx Ky xy][_ _ yx]. by apply: extensionality. - by move=> x y [ox oy _]; split => //;split => //. move=> x ale nex. have alo: ordinal_set x by move=> a /ale [h _]. move: (least_ordinal0 alo nex) => [ha hb hc]. exists (intersection x); hnf; rewrite (graph_on_sr ale); split=> // a ax. by apply /graph_on_P1; split => //; apply:hc. Qed. Lemma wordering_ole_pr x: ordinal_set x -> worder_on (ole_on x) x. Proof. move => osx. by apply: wordering_pr; [apply: wordering_ole | move => a /osx ox; split]. Qed. Lemma ole_order_r: order_r ordinal_le. Proof. exact: (proj1 wordering_ole). Qed. Lemma order_leR x: order x -> order_le x x. Proof. move=> ox; split => //; exists (identity (substrate x)); exists (substrate x). have ss:= (@sub_refl (substrate x)). have [pa pb]:=(iorder_osr ox ss). split => //;hnf;rewrite /bijection_prop identity_s identity_t pb. split => //; first by split => //;apply: identity_fb. hnf; aw; move=> z y xsr ysr; bw. symmetry; exact:(iorder_gleP x xsr ysr). Qed. Lemma oleR x: ordinalp x -> x <=o x. Proof. by move=> or; split. Qed. Hint Resolve oleR: fprops. Lemma oleT y x z: x <=o y -> y <=o z -> x <=o z. Proof. move: ole_order_r => [p1 p2 _]; apply: p1. Qed. Lemma oleA x y: x <=o y -> y <=o x -> x = y. Proof. move: ole_order_r => [p1 p2 _]; apply: p2. Qed. Lemma oleNgt x y: x <=o y -> ~(y ole [olt one]; case: one; apply: oleA. Qed. Lemma oltNge x y: x ~ (y <=o x). Proof. move => pa pb; exact:(oleNgt pb pa). Qed. Lemma olt_leT a b c: a b <=o c -> a [ab nab] bc; split; first by apply: (oleT ab bc). by dneg ac; rewrite -ac in bc; apply: oleA. Qed. Lemma ole_ltT b a c: a <=o b -> b a ab [bc nbc]; split; first by apply: (oleT ab bc). by dneg ca; rewrite ca in ab; apply: oleA. Qed. Lemma olt_ltT b a c: a b a [ab _] bc; apply: (ole_ltT ab bc). Qed. Lemma oleT_ell a b: ordinalp a -> ordinalp b -> [\/ a = b, a oa ob. case: (ordinal_trichotomy oa ob) => ha. - by constructor 2; apply/oltP. - by constructor 3; apply/oltP. - by constructor 1. Qed. Lemma oleT_el a b: ordinalp a -> ordinalp b -> a <=o b \/ b oa ob; case:(oleT_ell oa ob). - move ->; left; fprops. - by move => [h _]; left. - by right. Qed. Lemma oleT_ee a b: ordinalp a -> ordinalp b -> a <=o b \/ b <=o a. Proof. by move=> oa ob; case: (oleT_el oa ob); [by left | move => [h _]; right ]. Qed. Lemma oleT_si a b: ordinalp a -> ordinalp b -> (sub a b \/ inc b a). Proof. move=> oa ob; case: (oleT_el oa ob); first by move => [_ _]; left. by move/olt_i; right. Qed. (** Min and max *) Definition omax x y:= Yo (x <=o y) y x. Definition omin x y:= Yo (x <=o y) x y. Lemma OS_omax x y: ordinalp x -> ordinalp y -> ordinalp(omax x y). Proof. by move => ox oy; rewrite /omax;Ytac w. Qed. Lemma OS_omin x y: ordinalp x -> ordinalp y -> ordinalp(omin x y). Proof. by move => ox oy; rewrite /omin;Ytac w. Qed. Lemma omax_xy x y: x <=o y -> omax x y = y. Proof. by move => h; rewrite /omax; Ytac0. Qed. Lemma omax_yx x y: y <=o x -> omax x y = x. Proof. move => h; rewrite /omax; Ytac h1; [ apply:oleA h h1 | done ]. Qed. Lemma omin_xy x y: x <=o y -> omin x y = x. Proof. by move => h; rewrite /omin; Ytac0. Qed. Lemma omin_yx x y: y <=o x -> omin x y = y. Proof. move => h; rewrite /omin; Ytac h1; [ apply:oleA h1 h | done]. Qed. Lemma omaxC x y: ordinalp x -> ordinalp y -> omax x y = omax y x. Proof. move => ox oy. case: (oleT_ee ox oy) => h; first by rewrite omax_xy // omax_yx. rewrite omax_yx // omax_xy //. Qed. Lemma ominC x y: ordinalp x -> ordinalp y -> omin x y = omin y x. Proof. move => ox oy. case: (oleT_ee ox oy) => h; first by rewrite omin_xy // omin_yx. rewrite omin_yx // omin_xy //. Qed. Lemma omax_p1 x y: ordinalp x -> ordinalp y -> x <=o (omax x y) /\ y <=o (omax x y). Proof. move => ox oy. case: (oleT_ee ox oy) => h. rewrite (omax_xy h); split; fprops. rewrite (omax_yx h); split; fprops. Qed. Lemma omin_p1 x y: ordinalp x -> ordinalp y -> (omin x y) <=o x /\ (omin x y) <=o y. Proof. move => ox oy. case: (oleT_ee ox oy) => h. rewrite (omin_xy h); split; fprops. rewrite (omin_yx h); split; fprops. Qed. Lemma omax_p0 x y z: x <=o z -> y <=o z -> (omax x y) <=o z. Proof. by move => ha hb; rewrite /omax; Ytac h. Qed. Lemma omin_p0 x y z: z <=o x -> z <=o y -> z <=o (omin x y). Proof. by move => ha hb; rewrite /omin; Ytac h. Qed. Lemma omaxA x y z: ordinalp x -> ordinalp y -> ordinalp z -> omax x (omax y z) = omax (omax x y) z. Proof. move =>ox oy oz. case: (oleT_ee ox oy) => h1. rewrite (omax_xy h1); apply:omax_xy. exact: (oleT h1 (proj1 (omax_p1 oy oz))). rewrite (omax_yx h1); case: (oleT_ee ox oz) => h2. by rewrite (omax_xy (oleT h1 h2)). by rewrite (omax_yx (omax_p0 h1 h2)) (omax_yx h2). Qed. Lemma ominA x y z: ordinalp x -> ordinalp y -> ordinalp z -> omin x (omin y z) = omin (omin x y) z. Proof. move =>ox oy oz. case: (oleT_ee oy oz) => h1. rewrite (omin_xy h1); symmetry;apply:omin_xy. exact: (oleT (proj2 (omin_p1 ox oy)) h1). rewrite (omin_yx h1); case: (oleT_ee ox oy) => h2. by rewrite (omin_xy h2). rewrite (omin_yx h2) (omin_yx h1); apply:omin_yx; apply: (oleT h1 h2). Qed. Lemma ominmax x y z: ordinalp x -> ordinalp y -> ordinalp z -> omin x (omax y z) = omax (omin x y) (omin x z). Proof. move => ox; wlog: y z / y <=o z. move => H oy oz; case: (oleT_ee oy oz) => h; first by apply:H. by rewrite (omaxC oy oz) (H _ _ h oz oy) omaxC //; apply:OS_omin. move => yz oy oz;rewrite (omax_xy yz). symmetry; apply: omax_xy;case: (oleT_ee ox oy) => h1. rewrite (omin_xy h1) (omin_xy (oleT h1 yz)); fprops. by rewrite (omin_yx h1); apply:omin_p0. Qed. Lemma omaxmin x y z: ordinalp x -> ordinalp y -> ordinalp z -> omax x (omin y z) = omin (omax x y) (omax x z). Proof. move => ox; wlog: y z / y <=o z. move => H oy oz; case: (oleT_ee oy oz) => h; first by apply:H. by rewrite (ominC oy oz) (H _ _ h oz oy) ominC //; apply:OS_omax. move => yz oy oz;rewrite (omin_xy yz). symmetry; apply: omin_xy;case: (oleT_ee ox oy) => h1. by rewrite (omax_xy h1) (omax_xy (oleT h1 yz)). rewrite (omax_yx h1); exact:(proj1(omax_p1 ox (proj32 yz))). Qed. (** more least ordinal *) Lemma order_cp0 r r': order r -> order r' -> ((sub r r') <-> (forall x y, gle r x y -> gle r' x y)). Proof. move => or or'; split; first by move => h x y xy; apply: h. move => h t tr. move: ((proj41 or) _ tr) => p; move: tr; rewrite -p; apply:h. Qed. Lemma order_cp1 x y: worder x -> worder y -> sub x y -> (sub (substrate x) (substrate y) /\ x = (induced_order y (substrate x))). Proof. move => wo1 wo2 xy. move: (wo1) (wo2) => [o1 _] [o2 _]. have aa: sub (substrate x) (substrate y). move => t tsa; apply /(order_reflexivityP o2); apply: xy. by apply /(order_reflexivityP o1). have [sa sb]:=(iorder_osr o2 aa). split => //; apply: extensionality. move => t tx; apply /setI2_P; split; fprops. apply:sub_graph_coarse_substrate; fprops. move => t /setI2_P [ty /setX_P [pa pb pc]]; rewrite - pa. case: (proj2 (worder_total wo1) _ _ pb pc) => // h2. rewrite -pa in ty. move: (order_antisymmetry o2 (xy _ h2) ty) => h3; by move: h2; rewrite h3. Qed. Lemma order_cp2 x y: worder x -> worder y -> sub x y -> ordinal x <=o ordinal y. Proof. move => wo1 wo2 xy. have [pa pb]:= (order_cp1 wo1 wo2 xy). suff: order_le x y by move /(order_le_compatible1 wo1 wo2) /ordinal_le_P0. split; fprops; exists (identity (substrate x)), (substrate x); split => //. rewrite -pb; apply: identity_is; fprops. Qed. Lemma order_cp3 x y: worder x -> worder y -> ssub x y -> (segmentp y (substrate x)) -> ordinal x wo1 wo2 [xy xny] sp. split; first by apply: order_cp2. move => so. move: (ordinal_o_is wo2) (orderIS (ordinal_o_is wo1)); rewrite so => pa pb. move: (order_cp1 wo1 wo2 xy) => [ss xx]. move: (orderIT pa pb) => [f [sa sb [sc sd se] sf]]. have ff: function f by apply: bij_function. set g := Lf (fun z => Vf f z) (substrate y) (substrate y). have ta: lf_axiom (fun z => Vf f z) (substrate y) (substrate y). by move => t ty; apply: ss; rewrite - se; Wtac. have fg: function g by apply: lf_function. have sfsg: source f = source g by rewrite /g; aw. have gv: forall t, inc t (source g) -> Vf g t = Vf f t. rewrite /g; aw => t tf; aw. have rg: range (graph g) = substrate x. set_extens t; first by move/(range_fP fg) => [a ag ->];rewrite gv//; Wtac; ue. rewrite - se; move/ (proj2 (proj2 sc))=> [z]; rewrite sfsg => zg. move => <-; rewrite - (gv _ zg); apply/(range_fP fg); ex_tac. have pd: segmentp y (range (graph g)) by rewrite rg. have pc: order_morphism g y y. split => //; first by rewrite /g; split;aw. move => u v ug vg; rewrite (gv _ ug) (gv _ vg). rewrite - sfsg in ug vg; split; first by move/(sf u v ug vg); apply: xy. move => le1; move:(sf v u vg ug) => aux. move: (proj2 (proj1 sc) _ _ ug vg) => injf. rewrite sd in ug vg;case: (proj2 (worder_total wo2) _ _ ug vg) => // le2. have le3:gle y (Vf f v) (Vf f u) by move /aux: le2; apply: xy. by move: le2; rewrite (injf (order_antisymmetry (proj1 wo2) le1 le3)). move: rg; rewrite (unique_isomorphism_onto_segment wo2 pd pc). rewrite /identity; aw; rewrite identity_r => srr. by case: xny; rewrite xx - srr (iorder_substrate (proj1 wo2)). Qed. (** We study the properties of the least ordinal *) Lemma least_ordinal4 x (p: property) (y := least_ordinal p x): ordinalp x -> p x -> [/\ ordinalp y, p y & (forall z, ordinalp z -> p z -> y <=o z) ]. Proof. move=> ox px; move: (least_ordinal1 ox px) => [p1 p2 p3]. split => // t ot pt;move: (p3 _ ot pt) => zt; hnf;split => //. Qed. Lemma least_ordinal2 (p: property) x: (forall y, ordinalp y -> (forall z, z p z) -> p y) -> ordinalp x -> p x. Proof. move => h ox; ex_middle nx. move: (least_ordinal4 (p:= (fun z => ~ p z)) ox nx) => [p1 p2 p3]. case: p2; apply: h => // z zx. by ex_middle bad; move:(p3 _ (proj31_1 zx) bad) => /(oltNge zx). Qed. Lemma least_ordinal3 x (p: property) (y := least_ordinal (fun z => (~ p z)) x): ordinalp x -> ~ (p x) -> [/\ ordinalp y, ~(p y) & (forall z, z p z)]. Proof. move=> ox px. move: (least_ordinal4 (p:= (fun z => ~ p z)) ox px) => [p1 p2 p3]. split => // z zy. by ex_middle npz; move: (p3 _ (proj31_1 zy) npz) => /(oltNge zy). Qed. Lemma least_ordinal6 x (p:property) (y :=least_ordinal (fun z => ~ p z) x): ordinalp x -> p x \/ [/\ ordinalp y, forall z, inc z y -> p z & ~ p y]. Proof. move => oc; case: (p_or_not_p (p x)) => np; [by left | right]. move:(least_ordinal3 oc np) => [pa pb pc]; split => // z zy. by apply:pc; apply/(oltP pa). Qed. (** [union] is the supremum of a family of ordinals, cardinals or the predecessor of an ordinal. We study here the supremum of ordinals *) Notation "\osup" := union (only parsing). Notation "\csup" := union (only parsing). Definition opred := union. Definition cpred := union. Definition ordinal_ub E x:= forall i, inc i E -> i <=o x. Lemma OS_sup E: ordinal_set E -> ordinalp (\osup E). Proof. move=> alo; apply: ordinal_pr. apply: transitive_setU =>//. by move=> y yx; apply: ordinal_transitive; apply: alo. move=> y /setU_P [a ya ax]. exact: (ordinal_hi (alo _ ax) ya). Qed. Lemma ord_sup_ub E: ordinal_set E -> ordinal_ub E (\osup E). Proof. by move=> Ep i iE; split; [ apply: Ep | apply: OS_sup | apply: setU_s1]. Qed. Lemma ord_ub_sup E y: ordinalp y -> ordinal_ub E y -> \osup E <=o y. Proof. move => oy h; split => //. by apply:OS_sup => i /h /proj31. by move=> i /setU_P [z iz /h [_ _]]; apply. Qed. Lemma ord_sup_prop E: ordinal_set E -> exists! x, ordinalp x /\ (forall y, x <=o y <-> (ordinalp y /\ ordinal_ub E y)). Proof. move=> alo; set p := fun x: Set => _; apply /unique_existence;split. have ou:= (OS_sup alo). exists (\osup E); split => // y; split. move => h. have oy:= (proj32 h). split => //; move=> i iE; exact (oleT (ord_sup_ub alo iE) h). by move=> [oy aly]; apply:ord_ub_sup. have p1: forall x, p x -> ordinal_ub E x. move=> t [ox Ex]. by move: (oleR ox); rewrite (Ex t); move => [_]. have p2: forall x y, p x -> ordinalp y -> (ordinal_ub E y) -> x <=o y. move=> x1 y1 [ox opf] oy h; rewrite opf; split => //. move=> x y fx fy. exact: (oleA (p2 _ _ fx (proj1 fy) (p1 _ fy)) (p2 _ _ fy (proj1 fx) (p1 _ fx))). Qed. (** The empty set is the least ordinal *) Definition ord_zero := emptyset. Notation "\0o" := ord_zero. Lemma OS0: ordinalp \0o. Proof. move => y ye _ []; apply: extensionality; fprops. Qed. Lemma ozero_least x: ordinalp x -> \0o <=o x. Proof. move=> ox; split; fprops; apply: OS0. Qed. Lemma ord_ne0_pos x: ordinalp x -> x <> \0o -> \0o ox xnz; split; [ apply: ozero_least | apply nesym ]. Qed. Lemma ole0 x: x <=o \0o -> x = \0o. Proof. by move => [ _ _ /sub_set0]. Qed. Lemma olt0 x: x False. Proof. by move=> [/ole0 pa pab]. Qed. (** [osucc x] is the next ordinal after [x] *) Lemma osucc_pr x (z:= osucc x): ordinalp x -> x z <=o w). Proof. move=> ox; move: (OS_succ ox)=> oy. split; first by apply/oltP0; split => //; rewrite /z; fprops. move=> w /oltP0 [_ ow xw]. split => // t /setU1_P;case; last by move=> ->. by apply: (ordinal_transitive ow). Qed. Lemma oltS a: ordinalp a -> a oa; apply /oltP0; split;fprops. Qed. Lemma oleS a: ordinalp a -> a <=o (osucc a). Proof. by move=>/oltS []. Qed. Lemma oltSleP a b: a a <=o b. Proof. split. move /oltP0=> [p1 /OS_succr p2 p3]. by split => //; apply: ordinal_sub3. move => [p1 p2]; move/(ordinal_sub4P p1 p2) => q; apply/oltP0. split; fprops. Qed. Lemma oleSltP a b: a (osucc a) <=o b. Proof. split. by move => h; apply /(proj2 (osucc_pr (proj31_1 h))). move => [pa pb pc]; have asa:= (pc _ (setU1_1 a a)). apply /oltP0;split => //; exact:(ordinal_hi pb asa). Qed. Lemma oleSSP x y: (osucc x <=o osucc y) <-> x <=o y. Proof. split => h; last by apply /oleSltP /oltSleP. by apply /oltSleP /oleSltP. Qed. Lemma oltSSP x y: (osucc x (x h; last by apply /oltSleP /oleSltP. by apply /oleSltP /oltSleP. Qed. Definition osuccp x := exists2 y, ordinalp y & x = osucc y. Lemma osuccp_pr a: ordinalp a -> (exists b, a = osucc b) -> exists2 b, ordinalp b & a = osucc b. Proof. by move => oa [b bs]; exists b=> //; apply: OS_succr; rewrite - bs. Qed. Lemma opred_le x: ordinalp x -> opred x <=o x. Proof. move => ox;split; [ exact: (OS_sup (ordinal_set_ordinal ox)) | exact | ]. move => t /setU_P [y ty yx]; exact:(ordinal_transitive ox yx ty). Qed. Lemma osuccVidpred x: ordinalp x -> exactly_one (osuccp x) (x = opred x). Proof. move=> ox. case: (equal_or_not x (opred x)) => h. split; [by right | move=> [[y oy yt] _] ]. move: (succ_i y); rewrite - yt h => /setU_P [a ya]; rewrite yt. move/(oleP oy) => ay. by move/(oltP (proj31 ay)): ya => /oltNge. split; [left; apply:osuccp_pr => // | by case]. move: (opred_le ox) => la. exists (union x); apply: oleA; last by move/oleSltP: (conj la (nesym h)). split => //; [ exact: (OS_succ (proj31 la)) | move => t tx]. by move /oltSleP: (ord_sup_ub (ordinal_set_ordinal ox) tx) => /olt_i. Qed. (** a limit ordinal is a non-successor; it contains zero and is stable by [osucc]; it is the supremum of all elements smaller than itself *) Definition limit_ordinal x:= [/\ ordinalp x, inc \0o x & (forall y, inc y x -> inc (osucc y) x)]. Lemma limit_nonsucc x: limit_ordinal x -> x = opred x. Proof. move => [ox zx sx]. case: (proj1 (osuccVidpred ox)) => // [] [y oy xy]. have yx: (inc y x) by rewrite xy; fprops. by move: (sx _ yx); rewrite -xy => /(ordinal_irreflexive ox). Qed. Lemma limit_pos x: limit_ordinal x -> \0o [ox h _]; apply: ord_ne0_pos => // xz. by case: (@in_set0 \0o); move:h; rewrite xz. Qed. Lemma limit_nz x: limit_ordinal x -> x <> \0o. Proof. by move /limit_pos =>[_ /nesym]. Qed. Lemma limit_ordinal_P0 x: ordinalp x -> ((limit_ordinal x) <-> (nonempty x /\ x = opred x)). Proof. move=> ox; split. move => lx; move:(limit_nonsucc lx) => sa; split => //. by move: (proj32 lx) => zx; exists emptyset. move => [/nonemptyP nex ww]; split => //. exact: (olt_i (ord_ne0_pos ox nex)). move=> y yx; move: (ordinal_hi ox yx)=> oy. apply/(oltP ox);split; first by apply/oleSltP; apply/(oltP ox). move: (proj2 (osuccVidpred ox)) => dj h. case: dj; split => //; by exists y. Qed. Lemma ordinal_trichot x: ordinalp x -> [\/ x = \0o, osuccp x | limit_ordinal x]. Proof. move=> ox. case: (emptyset_dichot x); first by constructor 1. move=> nex. case: (proj1 (osuccVidpred ox)); first by constructor 2. by move=> xu; constructor 3; apply /(limit_ordinal_P0 ox). Qed. Lemma limit_ordinal_P x: limit_ordinal x <-> (\0o osucc t lx; split; first by apply: limit_pos. move:lx => [ox xnz xl]. by move => t /(oltP ox) => h; apply/(oltP ox); apply: xl. move =>[[sa xnz] sb];move: (proj32 sa) => ox; split => //. exact: (olt_i (ord_ne0_pos ox (nesym xnz))). by move => t /(oltP ox) h; apply/(oltP ox); apply: sb. Qed. Lemma succo_K y: ordinalp y -> opred (osucc y) = y. Proof. move=> oy; set_extens t => ts; last by apply: (setU_i ts); fprops. move: (setU_hi ts) => [a ta]; case /setU1_P;last by move => <-. move => ay;exact:(ordinal_transitive oy ay ta). Qed. Lemma predo_K x: osuccp x -> osucc (opred x) = x. Proof. by move=> [y oy xs]; rewrite xs (succo_K oy). Qed. (** If from two equipotent sets we remove an element, we get equipotent sets*) Section SuccProp. Variables (x y a b: Set). Hypotheses (nax: ~ inc a x) (nby: ~ inc b y). Lemma setU1_injective_card2: ((x +s1 a) \Eq (y +s1 b) <-> x \Eq y). Proof. split; last first. move=> [f [ [[ff injf] srjf] sf tf]]. have sjt: surjection (extension f a b) by apply: extension_fs =>//;ue. have st: source (extension f a b) = x +s1 a by rewrite /extension; aw;ue. have tt: target (extension f a b) = y +s1 b by rewrite /extension; aw;ue. have asf: ~ inc a (source f) by ue. exists (extension f a b); split => //. split => //; split; first by fct_tac. rewrite st; move=> u v; case /setU1_P=> us; case /setU1_P => vs. + rewrite ! extension_Vf_in //; try ue; apply: injf; ue. + rewrite (extension_Vf_in _ ff asf); last by ue. rewrite vs (extension_Vf_out _ ff asf);move =>h;case:nby;rewrite -h; Wtac. + rewrite us(extension_Vf_out _ ff asf)(extension_Vf_in _ ff asf);last by ue. move =>h; case: nby; rewrite h; Wtac. + rewrite us vs !extension_Vf_out //. move=> [f [[[ff injf] sjf] sf tf]]. have yt: inc b (target f) by rewrite tf; fprops. move: (proj2 sjf _ yt) => [a' asf Wa]. exists (Lf (fun z => Yo (z = a') (Vf f a) (Vf f z)) x y); split => //; aw. have xsf: inc a (source f) by rewrite sf; fprops. have sxsf: sub x (source f) by rewrite sf => t; fprops. apply: lf_bijective. + move=> z bx /=; Ytac ba. move: (Vf_target ff xsf); rewrite tf. case /setU1_P => // h; rewrite - h in Wa; move: (injf _ _ asf xsf Wa). by move=> ab; case: nax; rewrite -ab - ba. have bsf: inc z (source f) by rewrite sf; fprops. move: (Vf_target ff bsf); rewrite tf. case /setU1_P => // h; rewrite -h in Wa; move: (injf _ _ asf bsf Wa). by move=> ab; case: ba. + move=> u v ux vx; Ytac ua. Ytac va; first by rewrite ua va. move=> WW; move: (injf _ _ xsf (sxsf _ vx) WW) => aux. by rewrite -aux in vx. Ytac va; last by move=> ww;apply: (injf _ _ (sxsf _ ux) (sxsf _ vx) ww). move=> WW;move: (injf _ _ (sxsf _ ux) xsf WW) => aux. by case: nax; rewrite -aux. + move=> z zt. have ztf: (inc z (target f)) by rewrite tf ;fprops. case: (equal_or_not z (Vf f a)) => zW. rewrite zW; exists a' => //; last by Ytac0. move: asf; rewrite sf; case /setU1_P => //. by move=> ax;move: zt; rewrite zW -{1} ax Wa. move: ((proj2 sjf) _ ztf) => [b' bsf Wb]. case: (equal_or_not b' a') => ba. by move: nby; rewrite - Wa - ba Wb. exists b'; last by Ytac0. move: bsf; rewrite sf; case /setU1_P => // bx. by case: zW; rewrite -Wb bx. Qed. (** this says that a superset of an infinite set is infinite *) Lemma setU1_injective_card1: sub x y -> x \Eq (x +s1 a) -> y \Eq (y +s1 b). Proof. move=> sxy /EqS [f [[[ff injf] sjf] sf tf]]. have nbx: ~ inc b x by dneg bx; apply: sxy. apply:EqS. have Asf: inc a (source f) by rewrite sf; fprops. have wafx: inc (Vf f a) x by Wtac. set g := fun z => Yo (inc z x) (Vf f z) (Yo (z = b) (Vf f a) z). have Byp: forall t, inc t y -> t <> b by move=> t ty tB; case: nby; ue. have pa: lf_axiom g (y +s1 b) y. move=> t /setU1_P; rewrite /g; case. move=> ty; Ytac tx; first by apply: sxy; Wtac; rewrite sf; fprops. by move: (Byp _ ty) => aux; Ytac0. by move => ->; Ytac0; Ytac0; apply: sxy. have pb: forall u v, inc u (y +s1 b) -> inc v (y +s1 b) -> g u = g v -> u = v. move=> u v; rewrite /g; case /setU1_P => uy /setU1_P aux; last first. rewrite uy; Ytac0; Ytac0; Ytac vx. have vsf: inc v (source f) by rewrite sf; fprops. by move=> h; rewrite -(injf _ _ Asf vsf h) in vx. case:aux => vy //. by move: (Byp _ vy) => aux;Ytac0 => h; rewrite -h in vx. Ytac ux. Ytac vx; first by apply: injf; rewrite sf; fprops. case: aux => vy. move: (Byp _ vy) => aux; Ytac0=> h; case: vx; rewrite -h -tf. Wtac; rewrite sf; fprops. Ytac0 => aux. have usf: inc u (source f) by rewrite sf; fprops. by rewrite (injf _ _ usf Asf aux) in ux. have uB: u <> b by move => ub; case: nby; ue. Ytac0; Ytac vx. move=> h; rewrite h in ux; case: ux; rewrite -tf. Wtac; rewrite sf; fprops. case: aux => vy; [move: (Byp _ vy) => aux |]; Ytac0 => //. move=> h;case: ux; ue. exists (Lf g (y +s1 b) y); split; aw; apply: lf_bijective => // t ty. case: (inc_or_not t x) => tx. rewrite -tf in tx; move: ((proj2 sjf) _ tx)=> [z zsf wz]. move: zsf; rewrite sf;case /setU1_P => zx. exists z; first by apply /setU1_P; left; apply: sxy. by rewrite /g; Ytac0. by exists b; fprops; rewrite /g; Ytac0; Ytac0; rewrite - zx wz. by move: (Byp _ ty) => aux;exists t; fprops;rewrite /g; Ytac0; Ytac0. Qed. End SuccProp. (** We say that [x] is infinite if equipotent to its successor; finite otherwise; note that [ordinalp x] is missing in the definition of infinite *) Definition infinite_o u := u \Eq (osucc u). Definition finite_o u := ordinalp u /\ ~ (infinite_o u). Lemma OIS_in_inf x y: ordinalp y -> inc x y -> infinite_o x -> infinite_o y. Proof. rewrite /infinite_o => oy xy. have ox := (ordinal_hi oy xy). apply: setU1_injective_card1 (ordinal_irreflexive ox) (ordinal_irreflexive oy) (ordinal_transitive oy xy). Qed. Lemma OFS_in_fin x y: inc x y -> finite_o y -> finite_o x. Proof. move=> xy [oy niy]. have ox:=(ordinal_hi oy xy). by split => //; dneg nix; apply: (OIS_in_inf oy xy). Qed. Lemma succ_injective_oP x y: ordinalp x -> ordinalp y -> ((osucc x) \Eq (osucc y) <-> x \Eq y). Proof. move=> ox oy. apply: setU1_injective_card2 (ordinal_irreflexive ox) (ordinal_irreflexive oy). Qed. Lemma infinite_oP x: ordinalp x -> (infinite_o (osucc x) <-> infinite_o x). Proof. move=> ox; apply/ (succ_injective_oP ox (OS_succ ox)). Qed. Lemma finite_oP x: finite_o (osucc x) <-> finite_o x. Proof. split; move => [p1 p2]. have ox := (OS_succr p1). by move: p2 => /(infinite_oP ox) h. by split; [ apply: OS_succ | move/(infinite_oP p1)]. Qed. (** limit ordinals are infinite, since [osucc] is a bijecion for the least infinite ordinal *) Lemma OIS_limit x: limit_ordinal x -> infinite_o x. Proof. move=> xl. have ox:= (proj31 xl). move: (least_ordinal1 ox xl). set A := least_ordinal limit_ordinal x. move=> [oA [_ eA liA] leA]. suff p: (infinite_o A). case: (ordinal_sub oA ox (leA _ ox xl)) => Ax; first by ue. apply: (OIS_in_inf ox Ax p). have AA:=(ordinal_irreflexive oA). pose f z := Yo (inc z A) (osucc z) emptyset. apply:EqS;exists (Lf f (osucc A) A); split => //; aw. have q1: forall z, inc z (osucc A) -> inc (f z) A. by move=> u; case /setU1_P => hu; rewrite /f ?hu ; Ytac0 => //; apply: liA. apply: lf_bijective => //. move=> u v; rewrite /f; case /setU1_P => uA; [ | rewrite uA] => vA; Ytac0; case /setU1_P: vA => vA; rewrite ? vA; Ytac0. - exact: (ord_succ_inj (ordinal_hi oA uA) (ordinal_hi oA vA)). - move=> bad; empty_tac1 u. - move=> bad; symmetry in bad; empty_tac1 v. - done. move => y yA;have oy:= (ordinal_hi oA yA). case: (ordinal_trichot oy) => yv. - by exists A; fprops; rewrite /f (Y_false AA). - move:(yv) => [u ou uv]. have uA: inc u A by apply: (ordinal_transitive oA) (succ_i u); ue. by exists u; [ apply:(setU1_r _ uA) | rewrite /f (Y_true uA)]. - by move: (ordinal_irreflexive oy ((leA _ oy yv) y yA)). Qed. (** The cardinal of [x] is the least ordinal equipotent to [x] *) Definition cardinal x := (least_ordinal (equipotent x) (ordinal (worder_of x))). Definition cardinal_prop x y := [/\ ordinalp y, x \Eq y & (forall z, ordinalp z -> x \Eq z -> sub y z)]. Lemma cardinal_unique x y z: cardinal_prop x y -> cardinal_prop x z -> y = z. Proof. move=> [oy exy p1] [oz exz p2]. by apply: extensionality; [ apply: p1 | apply: p2 ]. Qed. Lemma cardinal_prop0 x: cardinal_prop x (cardinal x). Proof. have [wor sr] :=(proj1 (Zermelo_ter x)). have [or [_ _ [bf sf tf] ff]]:= (ordinal_isomorphism_exists wor). apply: (least_ordinal1 or); exists (ordinal_iso (worder_of x)). by split => //; ue. Qed. (* Module Type CardinalSig. Parameter cardinal : Set -> Set. Axiom cardinalE: cardinal = cardinalV. End CardinalSig. Module Cardinal: CardinalSig. Definition cardinal := cardinalV. Lemma cardinalE: cardinal = cardinalV. Proof. by []. Qed. End Cardinal. Notation cardinal := Cardinal.cardinal. Definition cardinalp x:= ordinalp x /\ (forall z, ordinalp z -> x \Eq z -> sub x z). Definition cardinal_fam x := allf x cardinalp. Definition cardinal_set X := alls X cardinalp. Lemma cardinalV_pr x: cardinalV_prop x (cardinal x). Proof. by rewrite Cardinal.cardinalE; apply /cardinalV_pr0. Qed. *) Definition cardinalp x:= ordinalp x /\ (forall z, ordinalp z -> x \Eq z -> sub x z). Definition cardinal_fam x := allf x cardinalp. Definition cardinal_set X := alls X cardinalp. Lemma cardinal_pr1 x: cardinal_prop x (cardinal x). Proof. by apply /cardinal_prop0. Qed. Lemma card_card x: cardinalp x -> cardinal x = x. Proof. move=> [cx1 cx2]. have aux: cardinal_prop x (cardinal x) by apply: cardinal_pr1. have aux': cardinal_prop x x by split; fprops. apply: (cardinal_unique aux aux'). Qed. Lemma CS_cardinal x: cardinalp (cardinal x). Proof. have [p1 p2 p3]:= (cardinal_pr1 x). split => // z oz ez; apply: (p3 _ oz (EqT p2 ez)). Qed. Lemma OS_cardinal x: cardinalp x -> ordinalp x. Proof. by move=> [ox _]. Qed. Hint Resolve CS_cardinal: fprops. Lemma double_cardinal x: cardinal (cardinal x) = cardinal x. Proof. apply: card_card; fprops. Qed. Lemma cardinal_pr0 x: x \Eq (cardinal x). Proof. exact: (proj32 (cardinal_pr1 x)). Qed. Lemma cardinal_pr x: (cardinal x) \Eq x. Proof. exact: (EqS (cardinal_pr0 x)). Qed. Lemma card_ord_le x: ordinalp x -> cardinal x <=o x. Proof. move => ox. move: (cardinal_pr1 x) => [pa pb pc]; split; fprops. Qed. Hint Resolve cardinal_pr0 cardinal_pr: fprops. Theorem card_eqP x y: (cardinal x = cardinal y) <-> (x \Eq y). Proof. move: (cardinal_pr1 x) (cardinal_pr1 y) => [ox exo lx][oy eyp ly]. split => h. apply: (EqT exo); rewrite h; exact: (cardinal_pr y). apply: extensionality. exact: (lx _ oy (EqT h eyp)). exact: (ly _ ox (EqT (EqS h) exo)). Qed. Lemma card_bijection f: bijection f -> cardinal (source f) = cardinal (target f). Proof. by move => bf; apply /card_eqP; exists f. Qed. Lemma cardinalP x: cardinalp x <-> (ordinalp x /\ forall z, inc z x -> ~ (x \Eq z)). Proof. rewrite /cardinalp; split; move=> [ox h]; split => //. move => z zx ne; move: ((h _ (ordinal_hi ox zx) ne) _ zx). apply: (ordinal_decent ox zx). move=> z oz exz. case: (ordinal_trichotomy oz ox) => ty; first by case: (h _ ty). by apply: (ordinal_transitive oz). by rewrite ty. Qed. Lemma cardinal_image f x : sub x (source f) -> injection f -> cardinal (Vfs f x) = cardinal x. Proof. by move => pa /(Eq_restriction1 pa)/card_eqP. Qed. Lemma cardinal_range f: injection f -> cardinal (range (graph f)) = (cardinal (source f)). Proof. by move /Eq_src_range /card_eqP. Qed. Lemma cardinal_indexed a b: cardinal (a *s1 b) = cardinal a. Proof. symmetry;apply /card_eqP; apply:Eq_indexed. Qed. Lemma cardinal_indexedr a b: cardinal (indexedr b a) = cardinal a. Proof. symmetry;apply /card_eqP; apply:Eq_rindexed. Qed. (* We define here zero one and two, and some notations *) Definition card_zero := emptyset. Definition card_one := singleton emptyset. Definition card_two := doubleton emptyset (singleton emptyset). Definition ord_one := card_one. Definition ord_two := card_two. Notation "\0c" := card_zero. Notation "\1c" := card_one. Notation "\2c" := card_two. Notation "\1o" := ord_one. Notation "\2o" := ord_two. Lemma osucc_zero: osucc \0o = \1o. Proof. set_extens z; last by move /set1_P => ->; fprops. move/setU1_P; case; [ case; case | move => ->//; apply:set1_1]. Qed. Lemma osucc_one: osucc \1o = \2o. Proof. set_extens z. case/setU1_P; [move/set1_P => ->; apply/set2_1 | move => ->; apply/set2_2]. by case /set2_P => h; apply /setU1_P; [left; apply /set1_P | right]. Qed. Corollary constants_v: (C0 = \0c /\ C1 = \1c /\ C2 = \2c). Proof. by []. Qed. Lemma OS1: ordinalp \1o. Proof. rewrite - osucc_zero; apply: OS_succ; apply: OS0. Qed. Lemma OS2: ordinalp \2o. Proof. rewrite - osucc_one; apply: OS_succ; apply: OS1. Qed. Lemma CS0: cardinalp \0c. Proof. by apply/cardinalP; split; [ apply: OS0 | move=> z /in_set0]. Qed. Lemma cardinal_set0: cardinal emptyset = \0c. Proof. apply:(card_card CS0). Qed. Lemma card_nonempty x: cardinal x = \0c -> x = emptyset. Proof. rewrite - cardinal_set0; move /card_eqP => [y [[[fy _] suy] sy ty]]. apply /set0_P => z zx; empty_tac1 (Vf y z); Wtac. Qed. Lemma card_nonempty0 x: x <> emptyset -> cardinal x <> \0c. Proof. by move => pa pb; case: pa; apply: card_nonempty. Qed. Lemma card_nonempty1 x: nonempty x -> cardinal x <> \0c. Proof. by move=> nex; apply :card_nonempty0; apply /nonemptyP. Qed. Lemma card1_nz: \1c <> \0c. Proof. fprops. Qed. Lemma card2_nz: \2c <> \0c. Proof. exact: (proj1 C2_ne_C01). Qed. Lemma card_12: \1c <> \2c. Proof. exact: (nesym (proj2 C2_ne_C01)). Qed. Hint Resolve card_12 card1_nz card2_nz: fprops. (** Zero is finite as well as its sucessors *) Lemma finite_zero: finite_o \0o. Proof. split; first by apply: OS0. move=> h; move: (EqS h); rewrite /card_zero=> h'. move/card_eqP:h'; rewrite cardinal_set0 => /card_nonempty h''. have [[]]: inc \0o emptyset by rewrite - h''; fprops. Qed. Lemma finite_one: finite_o \1o. Proof. rewrite - osucc_zero; apply /finite_oP; apply:finite_zero. Qed. Lemma finite_two: finite_o \2o. Proof. by rewrite - osucc_one; apply /finite_oP; apply:finite_one. Qed. Lemma finite_succ x: finite_o x <-> (x = emptyset \/ (exists2 y, finite_o y & x = osucc y)). Proof. split. move => fx; move: (fx) => [ox nix]. case: (ordinal_trichot ox); first by left. move=> [y oy xK]; rewrite xK; right; exists y => //. by move: fx; rewrite xK; move /finite_oP. move=> h; case: nix;apply: (OIS_limit h). case; first by move => ->; apply: finite_zero. by move=> [y fy ->];apply/finite_oP. Qed. Lemma gfunctions_empty X: (gfunctions emptyset X) = \1c. Proof. apply: set1_pr. apply/gfunctions_P2; bw; split; fprops; apply fgraph_set0. by move => z /gfunctions_P2 [_ /domain_set0_P]. Qed. (** If there is injections [E->F] and [F->E], then there are bijections; We start with the case [sub F E] *) Lemma Cantor_Bernstein1 E F f: sub F E -> (forall x, inc x E -> inc (f x) F) -> {inc E &, injective f} -> E \Eq F. Proof. move=> FE tf fi. set (A := Zo (powerset E)(fun x=> forall y, inc y x -> inc (f y) x)). have AE:sub A (powerset E) by apply: Zo_S. set (B:= E -s F). set (C:= Zo A (fun x=> sub B x)). have EC: inc E C. apply: Zo_i;[ apply: Zo_i; fprops;apply :setP_Ti | apply: sub_setC]. set (D:= intersection C). have p1: forall x, inc x C -> sub D x. move=> x xC t tD; apply: (setI_hi tD xC). have DA: inc D A. apply: Zo_i; first by apply /setP_P; apply: setI_s1. move=> y yD; apply: setI_i; first by ex_tac. move=> t tC; move: (setI_hi yD tC) => yt. by move: tC => /Zo_P [] /Zo_hi tp _; apply: tp. have DC: inc D C. apply: Zo_i => //t tD; apply /setI_i ; first by ex_tac. by move=> y /Zo_P [_]; apply. have BD: sub B D by move: DC => /Zo_P []. have cEB: (E -s B = F) by apply: setC_K. have Dst: (forall y, inc y D -> inc (f y) D) by move: DA => /Zo_P []. exists (Lf (fun y => Yo (inc y D) (f y) y) E F). aw;split => //; aw; apply: lf_bijective. move=> y yE /=; Ytac yD; first by apply: tf. rewrite -cEB; apply/setC_P; split => //; fprops. move=> u v uE vE; Ytac uD; Ytac vD => //; try (apply: fi => //). by move=> h; rewrite -h in vD; case: vD; apply: Dst. by move=> h; rewrite h in uD; case: uD; apply: Dst. move=> y yF; move: (yF); rewrite -cEB => /setC_P [yE nyB]. case: (inc_or_not y D) => yD; last by exists y => //; Ytac0. have DE:sub D E by move: DA => /Zo_P [] /setP_P. set (T:= D -s1 y). have BT: sub B T. by move=> t tB; apply /setC1_P; split; [ apply: BD | dneg ty; rewrite -ty]. have TA: (~ (inc T A)). move=> TA. by move: ((p1 _ (Zo_i TA BT)) _ yD) => /setC1_P [_]. have [x xT nfT]: exists2 x, inc x T & ~ (inc (f x) T). ex_middle bad; case: TA;apply: Zo_i => //. apply /setP_P; apply: sub_trans DE; apply: sub_setC. move=> z zT; case: (inc_or_not (f z) T) => //; move => nfzt; case:bad; ex_tac. move: xT => /setC1_P [xD nxy]. exists x; first by apply: DE. Ytac0;ex_middle fxy; case: nfT; apply /setC1_P; split; fprops. Qed. Theorem CantorBernstein X Y: (exists f, injection_prop f X Y) -> (exists f, injection_prop f Y X) -> (exists f, bijection_prop f X Y). Proof. move=> [f1 [[ff1 if1] sf1 tf1]][f2 [[ff2 if2] sf2 tf2]]. set Z := Vfs f2 Y. have e1: Y \Eq Z by apply: Eq_restriction1 => //; rewrite sf2; fprops. apply:EqT (EqS e1). pose g w := Vf f2 (Vf f1 w). move: (f_range_graph ff2) => rg2. move: (image_by_fun_source ff2); rewrite /Imf sf2 -/Z => zv. apply: (Cantor_Bernstein1 (f:=g)). - by rewrite zv -tf2; apply f_range_graph. - move=> x xs. apply/(Vf_image_P ff2); first by rewrite - sf2;fprops. exists (Vf f1 x) => //;Wtac. - rewrite - sf1 /g; move=> x y xs ys sg; apply: (if1 _ _ xs ys). apply: if2 => //;rewrite sf2 -tf1;Wtac. Qed. (** a finite ordinal is a cardinal ; so zero, one and two are cardinals *) Lemma CS_osucc x: finite_o x -> cardinalp (osucc x). Proof. move=> [ox nix]; apply/cardinalP; split; first by apply: OS_succ. move=> z zo aux1; case:nix; apply: EqT (EqS aux1). have zx: (sub z x). case /setU1_P:zo; [apply: (ordinal_transitive ox) | move=> ->; fprops]. have xx:= (ordinal_irreflexive ox). move: aux1 => [g [[[fg injg] sjg] sg tg]]. have p1: (forall t, inc t x -> inc (Vf g t) z). by rewrite -tg =>t tx; Wtac; rewrite sg; apply: setU1_r. have p2:(forall u v, inc u x -> inc v x -> Vf g u = Vf g v -> u = v). by move=> u v uE vE; apply: injg; rewrite sg ;apply: setU1_r. apply: (Cantor_Bernstein1 zx p1 p2). Qed. Lemma CS_finite_o x: finite_o x -> cardinalp x. Proof. rewrite finite_succ; case. move => ->; apply: CS0. by move=> [y yF ->]; apply: CS_osucc. Qed. Lemma CS1: cardinalp \1c. Proof. apply:CS_finite_o; apply:finite_one. Qed. Lemma CS2: cardinalp \2c. Proof. apply:CS_finite_o; apply:finite_two. Qed. Hint Resolve CS0 CS1 CS2 : fprops. (** We define finite and infinite for sets and cardinals *) Definition finite_c := finite_o. Definition infinite_c a := cardinalp a /\ infinite_o a. Definition finite_set E := finite_c (cardinal E). Definition infinite_set E := infinite_o (cardinal E). Lemma infinite_dichot1 x: finite_c x -> infinite_c x -> False. Proof. by move=> [_ pa][_ pb]. Qed. Lemma CS_finite2 x: finite_c x -> cardinalp x. Proof. by apply: CS_finite_o. Qed. Hint Resolve CS_finite2: fprops. Lemma infinite_dichot2 x : finite_c (cardinal x) -> infinite_set x -> False. Proof. move=> p1 p2; apply: (infinite_dichot1 p1); split; fprops. Qed. Lemma infinite_nz y: infinite_c y -> y <> \0c. Proof. move =>iy h; rewrite h in iy;case: (infinite_dichot1 finite_zero iy). Qed. Lemma infinite_card_limit1 x: infinite_c x -> opred x = x. Proof. move => icx. case: (osuccVidpred (OS_cardinal (proj1 icx))); case => // [] [y oy yz] _. have yy: (inc y x) by rewrite yz;fprops. move: icx => [ /cardinalP [oz cyp] iz]. case:(cyp _ yy); apply:EqS; rewrite yz. by apply/(infinite_oP oy); rewrite - yz. Qed. Lemma infinite_card_limit2 x: infinite_c x -> limit_ordinal x. Proof. move => ic; move: (ic) => [p1 p2]. apply/(limit_ordinal_P0 (proj1 (proj1 ic))). split; last by symmetry;apply: infinite_card_limit1. by case: (emptyset_dichot x) => // xe; case: (infinite_nz ic). Qed. (** We define here the cardinal successor *) Definition csucc x := cardinal (osucc x). Lemma CS_succ a: cardinalp (csucc a). Proof. rewrite /csucc; fprops. Qed. Lemma succ_zero: csucc \0c = \1c. Proof. rewrite /csucc osucc_zero; apply: card_card; apply: CS1. Qed. Lemma succ_one: csucc \1c = \2c. Proof. rewrite /csucc osucc_one; apply: card_card; apply: CS2. Qed. Lemma csucc_inf x: infinite_c x -> csucc x = x. Proof. by rewrite /csucc; move => [sa /card_eqP <-]; rewrite card_card. Qed. Lemma cardinal_irreflexive x: cardinalp x -> ~ (inc x x). Proof. move=> [ox _]; apply: (ordinal_irreflexive ox). Qed. Theorem succ_injective1: {when cardinalp &, injective csucc}. Proof. move=> a b ca cb; move /card_eqP. move: (CS_cardinal a) (CS_cardinal b) => cca ccb. move /(setU1_injective_card2(cardinal_irreflexive ca)(cardinal_irreflexive cb)). move /card_eqP; rewrite ! card_card //. Qed. Lemma csucc_pr a b: ~ (inc b a) -> cardinal (a +s1 b) = csucc (cardinal a). Proof. move=> bna; apply /card_eqP. apply /setU1_injective_card2 => //;last by fprops. apply: cardinal_irreflexive; fprops. Qed. Lemma csucc_pr1 a b: cardinal ((a -s1 b) +s1 b) = csucc (cardinal (a -s1 b)). Proof. rewrite csucc_pr //; apply: setC1_1. Qed. Lemma csucc_pr2 a b: inc b a -> cardinal a = csucc (cardinal (a -s1 b)). Proof. move=> ba; rewrite - {1} (setC1_K ba); apply: csucc_pr1. Qed. Lemma infinite_set_pr a b: inc b a -> a \Eq (a -s1 b) -> infinite_set a. Proof. move=> ba /card_eqP eq; apply/card_eqP; rewrite double_cardinal. move: (csucc_pr2 ba); rewrite -eq /csucc //. Qed. Lemma infinite_set_pr1 a b: inc b a -> a \Eq (a -s1 b) -> infinite_set (a -s1 b). Proof. move=> ab => h. move: (infinite_set_pr ab h). by move /card_eqP:h; rewrite /infinite_set; move => <-. Qed. Lemma infinite_set_pr2 x: infinite_o x -> ~(inc x x) -> infinite_set x. Proof. rewrite /infinite_o/osucc => /EqS eq1 eq2. have eq : (x +s1 x) -s1 x = x by apply: setU1_K. rewrite - eq; apply: infinite_set_pr1 ; [ fprops | ue ]. Qed. (** We exhibit an infinite set *) Lemma nat_infinite_set: infinite_set nat. Proof. have zn: inc (Ro 0) nat by apply: R_inc. set g := IM (fun y:nat => J (Ro y) (Ro (S y))). have p1: sgraph g by move=> t /IM_P [a <-]; fprops. have p0: fgraph g. split => // x y /IM_P [a <-] /IM_P [b <-]; aw => sp. by rewrite sp (R_inj sp). have p2: nat = domain g. set_extens t. move=> tn; apply/(domainP p1); exists (Ro (S (Bo tn))). apply/IM_P; exists (Bo tn); by rewrite B_eq. move=> /(domainP p1) [y] /IM_P [a Je]; rewrite -(pr1_def Je); apply: R_inc. have p3: range g = nat -s1 (Ro 0). set_extens t. move => /(rangeP p1) [x] /IM_P [a Jeq]. rewrite -(pr2_def Jeq); apply/setC1_P; split; first by apply: R_inc. by move=> h; move:(R_inj h). move=> /setC1_P [tn to]; apply/(rangeP p1). move:(B_eq tn); move:(Bo tn) => w wv. have: w <> 0 by dneg xx; ue. rewrite -wv;clear to wv. case: w => // n _; exists (Ro n); apply/IM_P; exists n =>//. apply: (infinite_set_pr zn). exists (triple nat (nat -s1 (Ro 0)) g); split; aw. have ff:function (triple nat (nat -s1 Ro 0) g). by apply:function_pr => //; rewrite - p3. split; last by apply: surjective_pr4 => //; aw. apply: injective_pr_bis =>// x x' y; aw. move => /IM_P [a J1] /IM_P [b J2]. rewrite -(pr1_def J1) - (pr1_def J2). move: (pr2_def J1)(pr2_def J2)=> r3 r4. by rewrite -r4 in r3; move: (R_inj r3)=> /eq_add_S ->. Qed. (** We consider here the least infinite ordinal; It is an infinite cardinal *) Definition omega0 := least_ordinal infinite_o (cardinal nat). Lemma omega0_pr: [/\ ordinalp omega0, infinite_o omega0 & (forall z, ordinalp z -> infinite_o z -> sub omega0 z)]. Proof. have p1: ordinalp (cardinal nat). by move: (CS_cardinal nat) => [ok _]. by move: (least_ordinal1 p1 nat_infinite_set). Qed. Lemma OS_omega: ordinalp omega0. Proof. exact: (proj31 omega0_pr). Qed. Hint Resolve OS0 OS1 OS2 OS_omega : fprops. Lemma OIS_omega: infinite_o omega0. Proof. exact: (proj32 omega0_pr). Qed. Lemma omega_P1 x: ordinalp x -> (infinite_o x <-> sub omega0 x). Proof. move=> ox; split; first by apply:(proj33 omega0_pr). move: OIS_omega OS_omega => bi oo sox. case: (ordinal_sub oo ox sox); first by move => <-. move=> h; apply: (OIS_in_inf ox h bi). Qed. Lemma omega_P2 x: inc x omega0 <-> finite_o x. Proof. split => xo. have ox:= (ordinal_hi OS_omega xo). split=>//; move /(omega_P1 ox) => h. case: (ordinal_irreflexive ox (h _ xo)). move: xo => [ox nifx]. by case:(oleT_si OS_omega ox) => // /(omega_P1 ox). Qed. Lemma CS_omega: cardinalp omega0. Proof. move: OS_omega => oo;split => // z oz pa; apply /(omega_P1 oz). by apply:(EqT (EqT (EqS pa) OIS_omega)); apply /succ_injective_oP. Qed. Lemma CIS_omega: infinite_c omega0. Proof. split; [ apply: CS_omega | apply: OIS_omega]. Qed. Lemma omega_limit0: omega0 = opred omega0. Proof. symmetry;apply:(infinite_card_limit1 CIS_omega). Qed. Lemma omega_limit: limit_ordinal omega0. Proof. exact:(infinite_card_limit2 CIS_omega). Qed. Lemma limit_ge_omega x: limit_ordinal x -> omega0 <=o x. Proof. move=> ln;move: OS_omega (ln) => oo [ox _ _]. by move /(omega_P1 ox):(OIS_limit ln); split. Qed. (** Some properties of infinite sets *) Lemma omega_limit3 x: infinite_c x -> sub omega0 x. Proof. by move => h;case:(limit_ge_omega (infinite_card_limit2 h)). Qed. Lemma infinite_setP x: infinite_set x <-> infinite_c (cardinal x). Proof. by move: (CS_cardinal x) => h; split; [ move => h1 | move => [] ]. Qed. Lemma infinite_set_pr3 x: omega0 <=o x -> infinite_c (cardinal x). Proof. move => [p1 p2 p3]. apply /infinite_setP;apply: infinite_set_pr2. apply /omega_P1 => //. exact (ordinal_irreflexive p2). Qed. End Bordinal. Export Bordinal. Module Cardinal. (** ** EIII-3-1 The cardinal of a set *) (** Singletons are equipotent, as well as doubletons *) Lemma set1_equipotent x y: singleton x \Eq singleton y. Proof. move: (setU1_injective_card2 (@in_set0 x) (@in_set0 y)); rewrite !set0_U2. by move => h; apply/h; apply: EqR. Qed. Lemma cardinal_set1 x: cardinal (singleton x) = \1c. Proof. rewrite -(card_card CS1); apply /card_eqP; apply:set1_equipotent. Qed. Lemma set2_equipotent x y: x <> y -> doubleton x y \Eq \2c. Proof. by move => /set2_equipotent_aux /proj31; set g := Lf _ _ _; exists g. Qed. Lemma cardinal_set2 x x': x <> x' -> cardinal (doubleton x x') = \2c. Proof. by move=> xx'; rewrite -(card_card CS2);apply /card_eqP /set2_equipotent. Qed. Lemma set_of_card_oneP x: cardinal x = \1c <-> singletonp x. Proof. split; last by move => [y ->]; apply:cardinal_set1. move/esym; rewrite -(card_card CS1); move /card_eqP; rewrite /card_one. move=> [f [[[ff injf] sf] srf <-]]; exists (Vf f emptyset). apply: set1_pr; first by Wtac; rewrite srf;fprops. move => z /(proj2 sf) [y]; rewrite srf; move=> /set1_P -> <-; fprops. Qed. Lemma set_of_card_twoP x: cardinal x = \2c <-> doubletonp x. Proof. split; last by move => [a [b [nab ->]]]; apply: cardinal_set2. move/esym;rewrite -(card_card CS2); move /card_eqP; rewrite / card_two. move=> [f [[[ff injf] sf] srf <-]]. have es: inc emptyset (source f) by rewrite srf; fprops. have ses: inc (singleton emptyset) (source f) by rewrite srf; fprops. exists (Vf f emptyset), (Vf f (singleton emptyset)); split. by move=> aux; move: (injf _ _ es ses aux); fprops. set_extens t => ts. move: (proj2 sf _ ts) => [z zsf <-]. move: zsf; rewrite srf; case /set2_P => ->; fprops. case /set2_P: ts => ->; Wtac. Qed. (** Equipotency is compatible with products *) Definition equipotent_ex E F := choose (fun z=> bijection_prop z E F). Lemma equipotent_ex_pr E F: E \Eq F -> bijection_prop (equipotent_ex E F) E F. Proof. move => e; apply: (choose_pr e). Qed. Definition fgraphs_equipotent x y := domain x = domain y /\ (forall i, inc i (domain x) -> (Vg x i) \Eq (Vg y i)). Lemma Eq_setXb x y: fgraphs_equipotent x y -> (productb x) \Eq (productb y). Proof. move=> [dxy ale]. pose g i := equipotent_ex (Vg x i) (Vg y i). pose f i := graph (g i). rewrite -(productb_gr x) - (productb_gr y) - dxy. exists (ext_map_prod (domain x) (Vg x) (Vg y) f). hnf; rewrite /ext_map_prod; split;aw. have ea: ext_map_prod_axioms (domain x) (Vg x) (Vg y) f. move=> i iI; move: (equipotent_ex_pr (ale _ iI))=> [[[fg _] _] sg tg]. rewrite /f; split; fprops. by rewrite - sg; apply: f_domain_graph. by rewrite -tg;apply: f_range_graph. split. apply: ext_map_prod_fi =>//. move=> i iI; move: (equipotent_ex_pr (ale _ iI)) => [[[fg ig] _] _]. rewrite /f; split; fprops;aw. apply: ext_map_prod_fs =>//. move=> i iI; move: (equipotent_ex_pr (ale _ iI)) => [[ig sg] _ p4]. by rewrite /f -p4; apply: surjective_pr3. Qed. Lemma Eq_setX a b a' b': a \Eq a' -> b \Eq b' -> (a \times b) \Eq (a' \times b'). Proof. move => [f [bf <- <-]] [f' [bf' <- <-]]. move:(ext_to_prod_fb bf bf') => h. exists (f \ftimes f'); split => //; rewrite /ext_to_prod; aw. Qed. Hint Resolve Eq_setX Eq_setXb: fprops. (** commutativity asssociativity distributivity of product equipotency *) Lemma product2A a b c: (a \times (b \times c)) \Eq ((a \times b) \times c). Proof. pose g z := J (J (P z) (P (Q z))) (Q (Q z)). apply:(@equipotent_aux g); apply: lf_bijective. move=> d /setX_P [pa pb] /setX_P [pc pd pe]. apply:setXp_i => //; apply:setXp_i => //. move=> u v /setX_P [pu Pu] /setX_P [pQu PQu QQu] /setX_P [pv Pv] /setX_P [pQv PQv QQv] eq. move:(pr1_def eq)(pr2_def eq)=> eq1 eq2. move:(pr1_def eq1)(pr2_def eq1)=> eq3 eq4. apply: pair_exten=>//; apply: pair_exten =>//. move => y /setX_P [py] /setX_P [pPy PP QP] Qc. exists (J (P (P y)) (J (Q (P y)) (Q y))) => //. apply:setXp_i => //; apply:setXp_i => //. by rewrite /g !(pr1_pair,pr2_pair) pPy py. Qed. (** Properties of disjoint sets *) Lemma disjointU2_pr0 a b x y: disjoint x y -> disjoint (a \times x) (b \times y). Proof. move=> dxy; apply: disjoint_pr. move=> u /setX_P [_ _ qx] /setX_P [_ _ qy]. apply: (nondisjoint qx qy dxy). Qed. Lemma disjointU2_pr1 x y: x <> y -> disjoint (singleton x) (singleton y). Proof. by move=> xy;apply: disjoint_pr; move => u /set1_P -> /set1_P. Qed. Lemma disjointU2_pr a b x y: x <> y -> disjoint (a *s1 x) (b *s1 y). Proof. by move=> xy; apply: disjointU2_pr0; apply: disjointU2_pr1. Qed. Hint Resolve disjointU2_pr: fprops. Lemma equipotent_disjointU X Y: fgraphs_equipotent X Y -> mutually_disjoint X -> mutually_disjoint Y -> (unionb X) \Eq (unionb Y). Proof. move=> [dXY ale] mX mY. pose g i := equipotent_ex (Vg X i) (Vg Y i). set X' := (Lg (domain X) (Vg X)). have pfX: partition_w_fam X' (unionb X). rewrite /X';split; fprops; bw. by hnf; bw; move => a b ax bx; bw; apply: mX. by rewrite (unionb_gr X). pose h i := change_target_fun (g i) (unionb Y). have fph: forall i, inc i (domain X')-> function_prop (h i)(Vg X' i) (unionb Y). rewrite /X'; bw; move=> i idx; bw. move: (equipotent_ex_pr (ale _ idx)) => [[[fg _] _] sg tg]. hnf;rewrite /h/change_target_fun; aw;split => //. apply: function_pr; fprops. apply: (@sub_trans (target (g i))). apply: f_range_graph=>//. rewrite tg; move=> t tf; union_tac; ue. rewrite f_domain_graph //. move:(extension_partition1 pfX fph). set x := common_ext _ _ _;move=> [[fx sx tx] agx']. have agx:forall i, inc i (domain X) -> agrees_on (Vg X i) x (h i). move: agx'; rewrite /X';bw => h1 i idx; move: (h1 _ idx); bw. exists x; split => //. split. split=>//. rewrite sx;move=> a b /setUb_P [i idX ai] /setUb_P [j jdX bj]. have ->: Vf x a = Vf (g i) a. move:(agx _ idX) => [_ _ ha];rewrite (ha _ ai) /Vf /h/change_target_fun; aw. have ->: Vf x b = Vf (g j) b. move:(agx _ jdX) => [_ _ hb];rewrite (hb _ bj) /Vf /h/change_target_fun; aw. move: (equipotent_ex_pr (ale _ idX)) => [[[fg ig] _] sg tg]. move: (equipotent_ex_pr (ale _ jdX)) => [[[fg' _] _] sg' tg']. have Wta: (inc (Vf (g i) a) (Vg Y i)) by rewrite -tg /g ; Wtac. have Wtb: (inc (Vf (g j) b) (Vg Y j)) by rewrite - tg' /g; Wtac. rewrite dXY in idX jdX. case: (mY _ _ idX jdX) => eq. rewrite -eq in bj |- * ; apply: ig; ue. move=> eq'; rewrite -eq' in Wtb. by red in eq;empty_tac1 (Vf (g i) a ). split => //. rewrite tx=> y /setUb_P; rewrite -dXY; move=> [i idX yV]. move: (equipotent_ex_pr (ale _ idX)) => [[_ sg] srg tg]. rewrite -tg in yV; move: ((proj2 sg) _ yV) => [z zsg Wg]. move: (agx _ idX)=> [s1 s2 v]. exists z; first by apply: s1; ue. rewrite srg in zsg; rewrite v// -Wg /Vf /h /change_target_fun; aw. Qed. Lemma equipotent_disjointU1 X Y: fgraphs_equipotent X Y -> (disjointU X) \Eq (disjointU Y). Proof. move=> [pc pd]. apply: equipotent_disjointU; rewrite /fgraphs_equipotent; fprops. split; rewrite/disjointU_fam -? dXY; fprops; bw. move=> i idy; bw; fprops; try ue. apply: (EqT (Eq_indexed2 (Vg X i) i) (EqT (pd _ idy) (Eq_indexed (Vg Y i) i))). Qed. Lemma union2Lv a b: a \cup b = unionb (variantLc a b). Proof. rewrite/unionb; bw; rewrite setUf2f. by rewrite variant_V_ca variant_V_cb. Qed. Lemma disjointLv a b: disjoint a b -> mutually_disjoint (variantLc a b). Proof. move=> db i j; bw => id1 jd; try_lvariant id1; try_lvariant jd; fprops. by right;apply:disjoint_S. Qed. Lemma equipotent_disjointU2 a b a' b': disjoint a b -> disjoint a' b' -> a \Eq a' -> b \Eq b' -> (a \cup b) \Eq (a' \cup b'). Proof. move=> dab dab' eqq' ebb'. rewrite ! union2Lv; apply:equipotent_disjointU; try apply: disjointLv =>//. hnf;bw; split => // i ind; try_lvariant ind. Qed. Definition doubleton_fam f a b := exists x y, [/\ x<>y, fgraph f, domain f = doubleton x y, Vg f x = a & Vg f y = b]. Lemma doubleton_fam_P f a b: doubleton_fam f a b <-> [/\ fgraph f, doubletonp (domain f) & range f = doubleton a b]. Proof. split. move => [x [y [xney fgf df fa fb]]]; split => //. by exists x,y. set_extens t. move/(range_gP fgf) =>[u udf ->]; move:udf; rewrite df. case/set2_P => ->; rewrite ?fa ? fb; fprops. case/set2_P => ->; apply/(range_gP fgf). exists x => //; rewrite df; fprops. exists y => //; rewrite df; fprops. move => [fgf [x [y [ xy df]]] rf]. have hx: inc (Vg f x) (doubleton a b). rewrite -rf;apply: (inc_V_range fgf); rewrite df; fprops. have hy: inc (Vg f y) (doubleton a b). rewrite -rf;apply: (inc_V_range fgf); rewrite df; fprops. have arf: inc a (range f) by rewrite rf; fprops. have brf: inc b (range f) by rewrite rf; fprops. move/(range_gP fgf):arf => [u udf fu]. move/(range_gP fgf):brf => [v vdf fv]. case:(equal_or_not (Vg f x) a) => fxa. exists x,y; split => //. move:vdf; rewrite df fv; case /set2_P => vv; rewrite vv => //. by case /set2_P:hy => fy;[ rewrite fy fxa |rewrite fy - vv]. case/set2_P:hx => // fxb. move:(nesym xy) => yx. exists y,x; rewrite set2_C; split => //. case/set2_P:hy => // fyb. by move:udf; rewrite df fu; case /set2_P => vv; rewrite vv // fxb. Qed. Lemma doubleton_fam_canon f: doubleton_fam (Lg C2 f) (f C0) (f C1). Proof. exists C0; exists C1; split => //;bw; fprops. Qed. Lemma two_terms_bij a b f (F:= variantLc a b) : doubleton_fam f a b -> exists g, [/\ bijection g, target g = domain F & f = F \cf (graph g)]. Proof. move => [x [y [xy fgf df fx fy]]]. move:(set2_equipotent_aux xy); set g := Lf _ _ _; move => [[bg sg tg] ga gb]. rewrite /F;exists g;split;fprops; first by aw; bw. move: (f_domain_graph (proj1 (proj1 bg))); rewrite sg => dg. apply: fgraph_exten; fprops. by rewrite /composef; bw; rewrite dg. rewrite /composef dg. rewrite df => z; case /set2_P => ->; rewrite /composef; bw; fprops. rewrite -/(Vf g x) ga; bw. rewrite -/(Vf g y) gb; bw. Qed. (** ** EIII-3-2 Order relation between cardinals *) Definition equipotent_to_subset x y:= exists2 z, sub z y & x \Eq z. Lemma eq_subset_ex_injP x y: equipotent_to_subset x y <-> (exists f, injection_prop f x y). Proof. rewrite/equipotent_to_subset; split. move=> [z zy [f [[injf srj] sf tf]]]. exists ((canonical_injection z y) \co f). hnf; rewrite /canonical_injection; aw; split => //. by apply: inj_compose1=>//; [apply: ci_fi=>// | aw]. move=> [f [injf srf tgf]]. exists (Imf f). rewrite -tgf; apply: fun_image_Starget; fct_tac. by rewrite /Imf - srf; apply:(Eq_restriction1 _ injf). Qed. Lemma eq_subset_pr2 a b a' b': a \Eq a' -> b \Eq b' -> equipotent_to_subset a b -> equipotent_to_subset a' b'. Proof. move=> /EqS [g [[injg _] sg tg]] [f [[injf _] sf tf]]. move/eq_subset_ex_injP => [h [ih sh th]]. apply /eq_subset_ex_injP; exists ((f \co h) \co g); split => //; aw. have ch: f \coP h by split => // ;try fct_tac; ue. apply: compose_fi => //. apply: compose_fi => //. split => //; try fct_tac; aw; ue. Qed. Lemma eq_subset_cardP x y: equipotent_to_subset x y <-> equipotent_to_subset (cardinal x) (cardinal y). Proof. move: (cardinal_pr x)(cardinal_pr y) => h1 h2. split => aux. apply: (eq_subset_pr2 (EqS h1)(EqS h2) aux). apply: (eq_subset_pr2 h1 h2 aux). Qed. Definition cardinal_le x y := [/\ cardinalp x, cardinalp y & sub x y]. Definition cardinal_lt a b := cardinal_le a b /\ a <> b. Notation "x <=c y" := (cardinal_le x y) (at level 60). Notation "x x <=o y. Proof. by move=> [[ox _] [oy _] le]. Qed. Lemma cardinal_le_aux1 x y: x <=c y -> equipotent_to_subset x y. Proof. move => [_ _ h]; exists x; fprops. Qed. Lemma cardinal_le_aux2P x y: cardinalp x -> cardinalp y -> (equipotent_to_subset x y <-> x <=c y). Proof. move=> cx cy. split; last by apply: cardinal_le_aux1. move => [z zy ezx]; split => //. move: (OS_cardinal cx)(OS_cardinal cy) => ox oy. case: (oleT_si ox oy) => // yx. suff eyz: (y \Eq z). move /card_eqP: (EqT ezx (EqS eyz)). rewrite (card_card cx) (card_card cy); move => -> //. move: ezx => [f [[[f0 f1] _] f2 f3]]. have syx:=(ordinal_transitive ox yx). have p1: forall t, inc t y -> inc (Vf f t) z. by move=> t ty; rewrite -f3; Wtac;rewrite f2; apply: syx. have p2: (forall u v, inc u y -> inc v y -> Vf f u = Vf f v -> u = v). by move=> u v ue ve; apply: f1; rewrite f2; apply: syx. apply: (Cantor_Bernstein1 zy p1 p2). Qed. Lemma eq_subset_cardP1 x y: equipotent_to_subset x y <-> (cardinal x) <=c (cardinal y). Proof. apply: (iff_trans (eq_subset_cardP x y)). split; first by move/cardinal_le_aux2P; apply; fprops. apply: cardinal_le_aux1. Qed. Lemma incr_fun_morph f: injection f -> (cardinal (source f)) <=c (cardinal (target f)). Proof. move=> injf; apply /eq_subset_cardP1. by apply/eq_subset_ex_injP; exists f. Qed. Lemma sub_smaller a b: sub a b -> (cardinal a) <=c (cardinal b). Proof. move=> ab; apply /eq_subset_cardP1; exists a; fprops. Qed. Lemma cleR x: cardinalp x -> x <=c x. Proof. by move=> cx;split. Qed. Hint Resolve cleR: fprops. Lemma cleT b a c: a <=c b -> b <=c c -> a <=c c. Proof. by move=> [ca cb eab] [_ cc ebc]; split => //; apply: sub_trans eab ebc. Qed. Lemma cleA x y: x <=c y -> y <=c x -> x = y. Proof. by move => [ca cb eab] [_ cc ebc]; apply: extensionality. Qed. Lemma cle_wor' E (x:= intersection E): cardinal_set E -> nonempty E -> inc x E /\ (forall y, inc y E -> x <=c y). Proof. move => sa sb. have sc: ordinal_set E by move => t /sa []. move: (ordinal_setI sb sc) => xe; split => //. by move => y yE; split; [apply: sa | apply: sa| apply:setI_s1]. Qed. Theorem cle_wor: worder_r cardinal_le. Proof. split => //. split => //. - move=> a b c;apply: cleT. - move=> a b; apply: cleA. - move=> x y [cx cy _]; split; fprops. move=> x xa xne. have xc: cardinal_set x by move=> b bx; move: (xa _ bx)=> [ok _]. have [ip ii]:=(cle_wor' xc xne); exists (intersection x). hnf; rewrite (graph_on_sr xa); split => //. by move=> u ux;move: (ii _ ux) => uy; apply graph_on_P1. Qed. (** The order on cardinals *) Lemma cle_eqVlt a b : a <=c b -> (a = b \/ a h1; case: (equal_or_not a b) => h2; [by left | by right ]. Qed. Lemma cleNgt a b: a <=c b -> ~(b ab [ba nba]; case: nba; apply: cleA. Qed. Lemma cltNge a b: a ~(b <=c a). Proof. move => ha hb; case: (cleNgt hb ha). Qed. Lemma clt_leT b a c: a b <=c c -> a [ab nab] bc; split; first exact: (cleT ab bc). by dneg ac; rewrite -ac in bc; apply: cleA. Qed. Lemma cle_ltT b a c: a <=c b -> b a ab [bc nbc]; split; first by exact: (cleT ab bc). by dneg ca; rewrite ca in ab; apply: cleA. Qed. Lemma clt_ltT a b c: a b a h1 [h2 _]; exact: (clt_leT h1 h2). Qed. Lemma wordering_cle_pr x: cardinal_set x -> (worder_on (graph_on cardinal_le x) x). Proof. move=> alc; apply: (wordering_pr cle_wor). move=> a ax; move: (alc _ ax); fprops. Qed. Lemma cleT_ell a b: cardinalp a -> cardinalp b -> [\/ a = b, a ca cb. move: (ca)(cb) => [oa _] [ob _]. case: (ordinal_trichotomy oa ob) => h. - by constructor 2; move: (ordinal_sub2 ob h) => [p1 p2]. - by constructor 3; move: (ordinal_sub2 oa h) => [p1 p2]. - by constructor 1. Qed. Lemma cleT_el a b: cardinalp a -> cardinalp b -> a <=c b \/ b ca cb; case: (cleT_ell ca cb). + move=> ->; left; fprops. + by move => [p1 _]; left. + by right. Qed. Lemma cleT_ee a b: cardinalp a -> cardinalp b -> a <=c b \/ b <=c a. Proof. move=> ca cb; case: (cleT_el ca cb); [by left | by move =>[p1 _]; right ]. Qed. (** Min and max *) Definition cmax x y:= Yo (x <=c y) y x. Definition cmin x y:= Yo (x <=c y) x y. Lemma CS_cmax x y: cardinalp x -> cardinalp y -> cardinalp(cmax x y). Proof. by move => ox oy; rewrite /cmax;Ytac w. Qed. Lemma CS_cmin x y: cardinalp x -> cardinalp y -> cardinalp(cmin x y). Proof. by move => ox oy; rewrite /cmin;Ytac w. Qed. Lemma cmax_xy x y: x <=c y -> cmax x y = y. Proof. by move => h; rewrite /cmax; Ytac0. Qed. Lemma cmax_yx x y: y <=c x -> cmax x y = x. Proof. move => h; rewrite /cmax; Ytac h1; [ apply:cleA h h1 | done]. Qed. Lemma cmin_xy x y: x <=c y -> cmin x y = x. Proof. by move => h; rewrite /cmin; Ytac0. Qed. Lemma cmin_yx x y: y <=c x -> cmin x y = y. Proof. move => h; rewrite /cmin; Ytac h1 ; [ apply:cleA h1 h | done]. Qed. Lemma cmaxC x y: cardinalp x -> cardinalp y -> cmax x y = cmax y x. Proof. move => ox oy. case: (cleT_ee ox oy) => h; first by rewrite cmax_xy // cmax_yx. rewrite cmax_yx // cmax_xy //. Qed. Lemma cminC x y: cardinalp x -> cardinalp y -> cmin x y = cmin y x. Proof. move => ox oy. case: (cleT_ee ox oy) => h; first by rewrite cmin_xy // cmin_yx. rewrite cmin_yx // cmin_xy //. Qed. Lemma cmax_p1 x y: cardinalp x -> cardinalp y -> x <=c (cmax x y) /\ y <=c (cmax x y). Proof. move => ox oy. case: (cleT_ee ox oy) => h. rewrite (cmax_xy h); split => //; fprops. rewrite (cmax_yx h); split => //; fprops. Qed. Lemma cmin_p1 x y: cardinalp x -> cardinalp y -> (cmin x y) <=c x /\ (cmin x y) <=c y. Proof. move => ox oy. case: (cleT_ee ox oy) => h. rewrite (cmin_xy h); split => //; fprops. rewrite (cmin_yx h); split => //; fprops. Qed. Lemma cmax_p0 x y z: x <=c z -> y <=c z -> (cmax x y) <=c z. Proof. by move => ha hb; rewrite /cmax; Ytac h. Qed. Lemma cmin_p0 x y z: z <=c x -> z <=c y -> z <=c (cmin x y). Proof. by move => ha hb; rewrite /cmin; Ytac h. Qed. Lemma cmaxA x y z: cardinalp x -> cardinalp y -> cardinalp z -> cmax x (cmax y z) = cmax (cmax x y) z. Proof. move =>ox oy oz. case: (cleT_ee ox oy) => h1. rewrite (cmax_xy h1); apply:cmax_xy. exact: (cleT h1 (proj1 (cmax_p1 oy oz))). rewrite (cmax_yx h1); case: (cleT_ee ox oz) => h2. by rewrite (cmax_xy (cleT h1 h2)). by rewrite (cmax_yx (cmax_p0 h1 h2)) (cmax_yx h2). Qed. Lemma cminA x y z: cardinalp x -> cardinalp y -> cardinalp z -> cmin x (cmin y z) = cmin (cmin x y) z. Proof. move =>ox oy oz. case: (cleT_ee oy oz) => h1. rewrite (cmin_xy h1); symmetry;apply:cmin_xy. exact: (cleT (proj2 (cmin_p1 ox oy)) h1). rewrite (cmin_yx h1); case: (cleT_ee ox oy) => h2. by rewrite (cmin_xy h2). rewrite (cmin_yx h2) (cmin_yx h1); apply:cmin_yx; apply: cleT h1 h2. Qed. Lemma cminmax x y z: cardinalp x -> cardinalp y -> cardinalp z -> cmin x (cmax y z) = cmax (cmin x y) (cmin x z). Proof. move => ox; wlog: y z / y <=c z. move => H oy oz; case: (cleT_ee oy oz) => h; first by apply:H. by rewrite (cmaxC oy oz) (H _ _ h oz oy) cmaxC //; apply:CS_cmin. move => yz oy oz;rewrite (cmax_xy yz). symmetry; apply: cmax_xy;case: (cleT_ee ox oy) => h1. rewrite (cmin_xy h1) (cmin_xy (cleT h1 yz)); fprops. by rewrite (cmin_yx h1); apply:cmin_p0. Qed. Lemma cmaxmin x y z: cardinalp x -> cardinalp y -> cardinalp z -> cmax x (cmin y z) = cmin (cmax x y) (cmax x z). Proof. move => ox; wlog: y z / y <=c z. move => H oy oz; case: (cleT_ee oy oz) => h; first by apply:H. by rewrite (cminC oy oz) (H _ _ h oz oy) cminC //; apply:CS_cmax. move => yz oy oz;rewrite (cmin_xy yz). symmetry; apply: cmin_xy;case: (cleT_ee ox oy) => h1. by rewrite (cmax_xy h1) (cmax_xy (cleT h1 yz)). rewrite (cmax_yx h1); exact:(proj1(cmax_p1 ox (proj32 yz))). Qed. Lemma ocle3 x y: cardinalp x -> cardinalp y -> x <=o y -> x <=c y. Proof. by move => cx cy [_ _ h]; split. Qed. Lemma oclt3 x y: cardinalp x -> cardinalp y -> x x cx cy [le ne]; split => //; apply: ocle3. Qed. Lemma cardinal_pr3 a: ordinalp a -> cardinal a <=o a. Proof. move => oa. have [h1 h2]:=(CS_cardinal a). by split => //; exact:(h2 _ oa (cardinal_pr a)). Qed. Lemma colt1 a x: cardinalp x -> inc a x -> cardinal a cx ax; apply: (oclt3 (CS_cardinal a) cx). move/(oltP (OS_cardinal cx)): (ax) => lt1; move:(proj31_1 lt1) => oa. exact:(ole_ltT (cardinal_pr3 oa) lt1). Qed. Lemma ocle1 x y: x <=o y -> (cardinal x) <=c (cardinal y). Proof. move => [pa pb pc]; apply /eq_subset_cardP1; exists x; fprops. Qed. Lemma oclt x y: x x [pa pb];split => //; apply: ocle. Qed. Lemma ocle2P x y: cardinalp x -> ordinalp y -> ((y (cardinal y cx oy; rewrite -{2} (card_card cx). move: cx => [ox xp]. split; move => [p1 p2]. move: (ocle1 p1) => p5; split => //; dneg p3. by apply: (oleA p1); split => //; apply: (xp _ oy); apply/card_eqP. case: (oleT_el ox oy) => // p3. move: (ocle1 p3)=> r1;case: p2; apply:cleA p1 r1. Qed. Lemma ordinals_card_ltP y: cardinalp y -> forall x, inc x y <-> (ordinalp x /\ (cardinal x) cy x; move: (proj1 cy) => oy. split. move /(oltP oy) => xy;move: (proj31_1 xy) => ox;split => //. by apply /(ocle2P cy ox). by move => [ox]; move /(ocle2P cy ox) /(oltP oy). Qed. Lemma finite_cP x: finite_c x <-> (cardinalp x /\ x <> csucc x). Proof. split => [ fx | [cx xsx]]. have cx: cardinalp x by fprops. split => //. move: fx => [p1 p2]; dneg h; apply /card_eqP. rewrite -/(csucc x) -h card_card//. split; first by apply: OS_cardinal. dneg infx; rewrite /csucc -{1} (card_card cx). by apply /card_eqP. Qed. Lemma infinite_cP x: infinite_c x <-> (cardinalp x /\ x = csucc x). Proof. rewrite /infinite_c /csucc/infinite_o. split; move=> [cx]. by rewrite -{4} (card_card cx); move /card_eqP=> aux. by rewrite -{1} (card_card cx); move /card_eqP=> aux. Qed. Lemma finite_dichot x: cardinalp x -> finite_c x \/ infinite_c x. Proof. move=> cx; case: (equal_or_not x (csucc x)) => h; [right | left]. by apply/infinite_cP. by apply/finite_cP. Qed. Lemma finite_dichot1 x: finite_set x \/ infinite_set x. Proof. by case: (finite_dichot (CS_cardinal x)); [ left | move/infinite_setP; right]. Qed. Lemma finite_lt_infinite a b: finite_c a -> infinite_c b -> a fa [cb]. have ca:= CS_finite2 fa. have ob:= (OS_cardinal cb). move/(omega_P1 ob) => ifb. by move: fa; move /omega_P2 /ifb => /(oltP ob) => /(oclt3 ca cb). Qed. Lemma finite_le_infinite a b: finite_c a -> infinite_c b -> a <=c b. Proof. move=> fa ib; exact: (proj1 (finite_lt_infinite fa ib)). Qed. Lemma ge_infinite_infinite a b: infinite_c a -> a <=c b -> infinite_c b. Proof. move => sa sb; case: (finite_dichot (proj32 sb)) => // fb. case:(cltNge (finite_lt_infinite fb sa) sb). Qed. Theorem le_finite_finite a b: finite_c b -> a <=c b -> finite_c a. Proof. move=> fb ab;case: (finite_dichot (proj31 ab)) => // ia. case: (cleNgt ab (finite_lt_infinite fb ia)). Qed. Lemma cardinal_fun_image t g : {inc t &, injective g} -> cardinal (fun_image t g) = cardinal t. Proof. move => H; symmetry; apply /card_eqP. exists (Lf g t (fun_image t g)); split;aw; apply /lf_bijective. + move=> s sa; apply /funI_P; ex_tac. + exact H. + by move => y /funI_P. Qed. Lemma sub_image_finite_set A B f: finite_set B -> (forall x, inc x A -> inc (f x) B) -> {inc A &, injective f} -> finite_set A. Proof. move => fsb fa fb. have: equipotent_to_subset A B. apply /eq_subset_ex_injP; exists (Lf f A B). by split; aw; apply: lf_injective. move /eq_subset_cardP=> es; apply:(le_finite_finite fsb). apply /cardinal_le_aux2P; fprops. Qed. Lemma succ_of_finite x: finite_o x -> csucc x = osucc x. Proof. by move=> cx; rewrite /csucc (card_card (CS_osucc cx)). Qed. Lemma infinite_c_P2 x: infinite_c x <-> (omega0 <=c x). Proof. move: CS_omega => h. rewrite /infinite_c /cardinal_le; split. by move=> [pa pb]; split => //; apply /(omega_P1 (OS_cardinal pa)). by move=> [pa pb pc]; split => //; apply /(omega_P1 (OS_cardinal pb)). Qed. Lemma sub_finite_set x y: sub x y -> finite_set y -> finite_set x. Proof. rewrite/finite_set=> xy fy; apply: (le_finite_finite fy (sub_smaller xy)). Qed. Section OrdinalFinite. Variable x:Set. Hypothesis ox: ordinalp x. Lemma ordinal_finite1: finite_set x -> finite_o x. Proof. move => fsx;split => //. move/(omega_P1 ox) => infc. apply:(infinite_dichot2 (sub_finite_set infc fsx)). hnf; rewrite (card_card CS_omega); exact OIS_omega. Qed. Lemma ordinal_finite2: infinite_set x -> infinite_o x. Proof. move=> ifs; ex_middle fo. by rewrite - (card_card (CS_finite_o (conj ox fo))). Qed. Lemma ordinal_finite3: finite_set x -> x ifs; apply /oltP0; split; fprops. by apply /omega_P2; apply: ordinal_finite1. Qed. Lemma ordinal_finite4: infinite_set x -> omega0 <=o x. Proof. by move=> ifs; split;fprops; apply /omega_P1 => //; apply: ordinal_finite2. Qed. End OrdinalFinite. (** Properties of 0 and 1 *) Lemma oge1P x: (\1o <=o x) <-> (\0o x <> \0o -> \1o <=o x. Proof. by move=> ox xne; apply/oge1P; apply: ord_ne0_pos. Qed. Hint Resolve oge1 : fprops. Lemma olt1 x: x x = \0o. Proof. by move/(oltP OS1) /set1_P. Qed. Lemma olt2 a: a a = \0o \/ a = \1o. Proof. by move/(oltP OS2)/set2_P. Qed. Lemma ozero_dichot x: ordinalp x -> x = \0o \/ \0o ox; case: (equal_or_not x \0o) => xe; first by left. by right; apply: ord_ne0_pos. Qed. Lemma oone_dichot x y: x (y = \1o \/ \1o h; case: (equal_or_not y \1o) => h'; [by left | right; split; fprops]. apply: oge1; [exact : (proj32_1 h) | move=> h''; case: (@olt0 x); ue]. Qed. Lemma czero_least x: cardinalp x -> \0c <=c x. Proof. move=> cx; rewrite - cardinal_set0 - (card_card cx). apply: sub_smaller; fprops. Qed. Lemma cle0 a: a <=c \0c -> a = \0c. Proof. move=> alez; exact:(cleA alez (czero_least (proj31 alez))). Qed. Lemma clt0 x: x False. Proof. by move=> [pa pab]; move: (cle0 pa). Qed. Lemma card_ne0_pos x: cardinalp x -> x <> \0c -> \0c cx xnz; split => //; [ by apply: czero_least | fprops]. Qed. Lemma card_gt_ne0 x y: x y <> \0c. Proof. move => xy yz; rewrite yz in xy; exact: (clt0 xy). Qed. Lemma succ_nz n: csucc n <> \0c. Proof. apply: card_nonempty1; exists n; fprops. Qed. Lemma succ_positive a: \0c [res _]. Qed. Lemma cle_12: \1c <=c \2c. Proof. by split; fprops => // t /set1_P ->; apply:set2_1. Qed. Lemma clt_12: \1c (\0c le1;first exact:(clt_leT (clt_01) le1). by apply: (ocle3 CS1 (proj32_1 le1)); apply /oge1P; exact: (oclt le1). Qed. Lemma clt1 x: x x = \0c. Proof. by move=> /oclt/olt1. Qed. Lemma cge1 x: cardinalp x -> x <> \0c -> \1c <=c x. Proof. by move => sa sb; apply /cge1P; apply:card_ne0_pos. Qed. Lemma clt2 a: a a = \0c \/ a = \1c. Proof. by move/oclt/olt2. Qed. Lemma cge2 x: cardinalp x -> x <> \0c -> x <> \1c -> \2c <=c x. Proof. by move => cx x0 x1; case: (cleT_el CS2 cx) => //;case /clt2. Qed. Lemma cle1P E: \1c <=c (cardinal E) <-> nonempty E. Proof. split. move => h; case: (emptyset_dichot E) => // h1. case:(cleNgt h); rewrite h1 (cardinal_set0); exact:clt_01. move=> /card_nonempty1 nE; apply: cge1;fprops. Qed. Lemma cle2P E: \2c <=c (cardinal E) <-> exists a b, [/\ inc a E, inc b E & a <> b]. Proof. split. rewrite - (card_card CS2) => /cardinal_le_aux1/(eq_subset_cardP \2c). move => [x xE] => /card_eqP; rewrite (card_card CS2) => /esym. move/set_of_card_twoP => [a [b [anb xv]]]. exists a,b; split => //; apply: xE; rewrite xv; fprops. move => [x [y [xE yE nxy]]]. have sE: (sub (doubleton x y) E) by move=> t td; case/set2_P: td =>->; fprops. by rewrite - (cardinal_set2 nxy); apply: sub_smaller. Qed. (** There is a set containing all cardinals less or equal a. Each family of cardinals has an upper bound *) Definition cardinals_le a:= Zo (osucc a) cardinalp. Definition cardinals_lt a:= Zo a (fun b => b forall b, (inc b (cardinals_le a) <-> (b <=c a)). Proof. move=> ca b; rewrite/cardinals_le; split. move /Zo_P => [/(oleP (proj1 ca)) bs cb];exact:(ocle3 cb ca bs). move => lba;apply: Zo_i; first by apply /(oleP (proj1 ca))/(ocle lba). exact: (proj31 lba). Qed. Lemma cardinals_ltP a: cardinalp a -> (forall b, inc b (cardinals_lt a) <-> (b cx y; split; first by move /Zo_P => [bs cb]. by move => h; move: (oclt h) => /(oltP0) [ _ _ yx]; apply /Zo_i. Qed. Lemma cardinals_le_alt a: cardinalp a -> (cardinals_le a) = fun_image (powerset a) cardinal. Proof. move => h; set_extens t. move/(cardinals_leP h) => ha. move/cardinal_le_aux1: (ha) => [y /setP_P yx /card_eqP exy]; apply /funI_P. by ex_tac; rewrite - (card_card (proj31 ha)). move/funI_P => [z /setP_P /sub_smaller ha ->]; apply /(cardinals_leP h). by rewrite - (card_card h). Qed. Lemma CS_sup E: cardinal_set E -> cardinalp (\csup E). Proof. move=> alc. have os: ordinal_set E by move=> t /alc/proj1. have oe:= (OS_sup os). apply /cardinalP; split => // z zE /card_eqP ezE. have oz:=(ordinal_hi oe zE). have [a ax za]: exists2 a, inc a E & inc z a. ex_middle h. have p2: (forall a, inc a E -> a <=o z). move=> a ax;move: (os _ ax) => oa;split => //. case:(oleT_si oa oz) => // za; case: h; ex_tac. case: (ordinal_irreflexive oz (proj33 (ord_ub_sup oz p2) _ zE)). have oa := (os _ ax). have cza : a \Eq z. apply/card_eqP; apply:cleA. - by move: (sub_smaller (proj33 (ord_sup_ub os ax))); rewrite ezE. - exact (sub_smaller (ordinal_transitive (os _ ax) za)). case:(ordinal_irreflexive oz((proj2 (alc _ ax) _ oz cza) _ za)). Qed. Lemma card_ub_sup E y: cardinalp y -> (forall i, inc i E -> i <=c y) -> \csup E <=c y. Proof. move => cy ali. have csE: cardinal_set E by move => i /ali []. have: (\csup E) <=o y by apply: (ord_ub_sup (proj1 cy)) => o /ali/ocle. by move /ocle1; rewrite (card_card (CS_sup csE)) (card_card cy). Qed. Lemma card_sup_ub E: cardinal_set E -> forall i, inc i E -> i <=c \csup E. Proof. move => h; move: (CS_sup h) => cs. have os: ordinal_set E by move=> t tx; move: (h _ tx) => [ct _]. move=> i ie; move: (ord_sup_ub os ie)=> [pa pb pc]; split; fprops. Qed. Lemma card_sup_image E f g: (forall x, inc x E -> f x <=c g x) -> \csup (fun_image E f) <=c \csup (fun_image E g). Proof. move => h. have pb: cardinal_set (fun_image E g). by move => t /funI_P [z zE ->]; case: (h _ zE). apply: card_ub_sup => //; first by apply: CS_sup. move=> i /funI_P [z zE ->]; apply: (cleT (h _ zE)). apply: card_sup_ub => //; apply/funI_P; ex_tac. Qed. Lemma cardinal_supremum1 x: cardinal_set x -> exists! b, [/\ cardinalp b, (forall a, inc a x -> a <=c b) & (forall c, cardinalp c -> (forall a, inc a x -> a <=c c) -> b <=c c)]. Proof. move=> alc. move: (CS_sup alc) (card_sup_ub alc) => pa pb. apply /unique_existence; split. by exists (union x); split => // y cy; apply:(card_ub_sup). move=> u v [cu up1 up2][cv vp1 vp2]. exact: (cleA (up2 _ cv vp1) (vp2 _ cu up1)). Qed. Theorem cardinal_supremum2 x: fgraph x -> cardinal_fam x -> exists!b, [/\ cardinalp b, (forall a, inc a (domain x) ->(Vg x a) <=c b) & (forall c, cardinalp c -> (forall a, inc a (domain x) -> (Vg x a) <=c c) -> b <=c c)]. Proof. move=> fg alx. have aly: cardinal_set (range x). by move=> a /(range_gP fg) [z zd ->]; apply: alx. move /unique_existence: (cardinal_supremum1 aly) => [[b [cb bp1 bp2]] _]. apply /unique_existence;split. exists b; split =>//. move=> a adx; apply: bp1; by apply: inc_V_range. move=> c cc hc; apply: bp2=> //. move=> a => /(range_gP fg) [d dd ->]. by apply: hc. move=> u v [cu up1 up2][cv vp1 vp2]. exact:(cleA (up2 _ cv vp1) (vp2 _ cu up1)). Qed. Lemma surjective_cle x y: (exists z, surjection_prop z x y) -> cardinal y <=c cardinal x. Proof. move=> [z [sjz sz tz]]. apply /eq_subset_cardP1. move: (exists_right_inv_from_surj sjz) => [f ri]. have ii:=(right_inverse_fi ri). have si:= (right_i_source ri). move: ri=> [[_ _ ti] _]. rewrite -tz - sz - si ti. by apply /eq_subset_ex_injP; exists f. Qed. Lemma image_smaller f: function f -> cardinal (Imf f) <=c cardinal (source f). Proof. move=> ff. have sr:=(restriction_to_image_fs ff). apply: surjective_cle. exists (restriction_to_image f). by split=>//; rewrite/ restriction_to_image /restriction2; aw. Qed. Lemma image_smaller1 f x: function f -> cardinal (Vfs f x) <=c cardinal x. Proof. move => pa. move: (@subsetI2l x (source f)) (@subsetI2r x (source f)) => a1 a2. have ->: Vfs f x = Vfs f (x \cap (source f)). set_extens t => /dirim_P [u p1 p2]; apply /dirim_P; exists u => //. apply /setI2_P;split => //; Wtac. by apply: a1. move: (restriction1_fs pa a2) (sub_smaller a1) => sjb le1. move: (image_smaller (proj1 sjb)). rewrite (surjective_pr0 sjb) /restriction1; aw => le2; apply:cleT le2 le1. Qed. Lemma range_smaller f: fgraph f -> cardinal (range f) <=c cardinal (domain f). Proof. move=> fgf. have ff: (function (triple (domain f) (range f) f)). by apply: function_pr; fprops. have ->: (range f = Imf (triple (domain f)(range f) f)). by rewrite (image_by_fun_source ff); aw. move:(image_smaller ff); aw. Qed. Lemma fun_image_smaller a f: cardinal (fun_image a f) <=c cardinal a. Proof. have sjb: (surjection (Lf f a (fun_image a f))). apply: lf_surjective; first by move=> t ta; apply /funI_P; ex_tac. by move=> y /funI_P. move: (image_smaller (proj1 sjb)); rewrite (surjective_pr0 sjb); aw. Qed. End Cardinal. Export Cardinal.