Library sset7
Theory of Sets EIII-3 Equipotents Sets. Cardinals
Copyright INRIA (2009-2013) Apics; Marelle Team (Jose Grimm).Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset6.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module Bordinal.
Definition transitive_set X:= forall x, inc x X -> sub x X.
Definition decent_set x := forall y, inc y x -> ~ (inc y y).
Definition trans_dec_set X := transitive_set X /\ decent_set X.
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 succ_o x := x +s1 x.
Lemma transitive_setU x: (alls x transitive_set)
-> transitive_set (union x).
Proof.
move=> alt a au t ta; move: (setU_hi au)=> [y ay yx].
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.
apply: transitive_setU => y yx; exact (proj1 (alt _ yx)).
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).
move=> y yx; apply: ((proj1 (alt _ yx)) _ (setI_hi au yx)) =>//.
move=> a au aa; move: nea => [y yx].
by apply: ((proj2 (alt _ yx)) _ (setI_hi au yx)).
Qed.
Lemma succ_i x: inc x (succ_o 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 (succ_o y).
Proof.
move => [pa pb]; split.
move => z /setU1_P; case.
by move => zy t tz; move: ((pa _ zy) _ tz) => 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.
move: (ox _ sux (proj1 tct) ntx)=> ux.
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 => ox; move: (ordinal_trans_dec ox)=> []. Qed.
Lemma ordinal_decent x: ordinalp x -> decent_set x.
Proof. by move => ox; move: (ordinal_trans_dec ox)=> []. 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; apply: oy => //; apply: (ordinal_transitive ox).
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: (dy _ xy) => ab; dneg ac; rewrite {2} ac.
Qed.
Lemma ordinal_sub3 x y: ordinalp y ->
inc x (succ_o 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 (succ_o 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) => //.
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 (succ_o 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 => //.
move=> tx; case: yntxx; apply: extensionality=>// => s; case /setU1_P => sx.
by rewrite tx in ty; move: (tsy _ ty); 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 (succ_o x) -> ordinalp x.
Proof. move=> os ; apply: (ordinal_hi os); fprops. Qed.
Ltac ord_tac0 :=
match goal with
| h1: ordinalp ?a, h2: inc ?b ?a |- ordinalp ?b =>
apply: (ordinal_hi h1 h2)
| h1: ordinalp ?x, h2: inc ?y ?x, h3: inc ?z ?y |- inc ?z ?x =>
apply: (((ordinal_transitive h1) _ h2) _ h3)
end.
Lemma non_collectivizing_ordinal:
~(exists x, forall a, ordinalp a -> inc a x).
Proof.
move=> [x xp]; set (y := Zo x ordinalp).
have osy: ordinal_set y by move => t /Zo_hi.
have oo: forall a, ordinalp a -> inc a y.
by move => a oa; apply: Zo_i => //; apply: xp.
have yo: ordinalp y.
apply: ordinal_pr => // a ay b ba.
apply: (oo _ (ordinal_hi (osy _ ay) ba)).
case: (ordinal_irreflexive yo (oo _ yo)).
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 h1: ordinalp x by ord_tac0.
have: inc x x by ord_tac0.
by apply: ordinal_irreflexive.
Qed.
Lemma ord_succ_inj : { when ordinalp &, injective succ_o }.
Proof.
move=> a b oa ob eq.
have : inc a (succ_o b) by rewrite -eq; fprops.
case /setU1_P => // ab.
have : inc b (succ_o a) by rewrite eq; fprops.
case /setU1_P => // ba.
case: (ordinal_irreflexive oa (ordinal_transitive oa ba ab)).
Qed.
Lemma ordo_leP a b c:
gle (ordinal_o a) b c <-> [/\ inc b a, inc c a & sub b c].
Proof. apply: sub_gleP. Qed.
Lemma ordo_ltP a b c: ordinalp c -> inc a c -> inc b c ->
(glt (ordinal_o c) a b <-> inc a b).
Proof.
move=> oc ac bc.
move: (ordinal_hi oc bc) => ob.
split.
move => [] /ordo_leP [h1 h2 h3] h4.
by case: (ordinal_sub (ordinal_hi oc ac) ob h3).
move=> ab; move: (ordinal_sub2 ob ab)=> [h1 h2].
by 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 (succ_o 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=> bx px.
set (t:= Zo (succ_o x) p).
have xt: inc x t by apply /Zo_i; fprops.
have net: nonempty t by exists x.
have alo: (ordinal_set t) by move :(OS_succ bx) => aux a /Zo_S ak; ord_tac0.
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 bx oz) => ty.
- by apply: (sub_trans sxt); apply: (ordinal_transitive oz).
- 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 => //.
apply: ordinal_sub3 => //; by 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.
move: (sub_osr x) => [pa pb].
rewrite /ordinal_o; split => //; rewrite pb.
move=> y yE nex.
have p1: (ordinal_set y) by move=> a ax; move: (yE _ ax) => aE; ord_tac0.
have hh: sub y (substrate (sub_order x)) by ue.
have ix:= (ordinal_setI nex p1).
rewrite /least; aw;ex_tac.
move=> z zy; apply/iorder_gleP => //.
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).
rewrite sg; move=> eXE; contradiction.
rewrite sg; move=> [x xs ->]; rewrite ordinal_segment1 //.
Qed.
Lemma ordinal_o_sr E: substrate (ordinal_o E) = E.
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: (wor)=> [or worp].
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; rewrite (vf1 _ _ aE); exists b.
have BE: (sub Bad E) by rewrite /Bad; apply: Zo_S.
move: (worp _ BE h) => [y []];aw; move=> /Zo_P [yE iWWy] yp.
move: (iWWy); rewrite (vf1 _ _ yE); move=> [u us Wu].
have badu: inc u Bad by apply: Zo_i=>//; [rewrite /E;order_tac | ue ].
move: (iorder_gle1 (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.
rewrite (vf1 _ _ bE)(vf1 _ _ aE); move=> [u us h]; 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; rewrite (vf1 _ _ zs).
move=> [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: (worp _ sBE h) => [x []]; aw; move => /Zo_P [xE ioWx] xp.
case: ioWx; apply: ordinal_pr.
move=> b; rewrite (vf1 _ _ xE).
move=> [u [ua _] Wu] t tb; move: (incf _ _ ua); apply; ue.
move => a; rewrite (vf1 _ _ xE); move=> [u usr <-].
ex_middle h'.
have ub:inc u Bad by apply: Zo_i => //; rewrite /E;order_tac.
move: (iorder_gle1 (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.
by move=> wor; move:(ordinal_isomorphism_exists wor) => [h _].
Qed.
Lemma ordinal_o_is r: worder r -> r \Is (ordinal_o (ordinal r)).
Proof.
move=> wor; move:(ordinal_isomorphism_exists wor) => [_ h].
by exists (ordinal_iso r).
Qed.
Lemma ordinal_o_o E: ordinalp E -> ordinal (ordinal_o E) = E.
Proof.
move=> oE; move: (ordinal_o_wor oE)=> woi.
move: (ordinal_isomorphism_exists woi) => [_ ] h.
by move: (ordinal_isomorphism_unique oE (OS_ordinal woi) h) => [res _].
Qed.
Lemma ordinal_o_isu x y:
ordinalp x -> ordinalp y ->
(ordinal_o x) \Is (ordinal_o y) -> x = y.
Proof.
by move=> ox oy [f fi]; move: (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.
apply: (ordinal_o_isu o1 o2 (orderIT (orderIT (orderIS i1) or) i2)).
Qed.
Lemma ordinal_o_isu2 r E: worder r -> ordinalp E ->
r \Is (ordinal_o E) -> ordinal r = E.
Proof.
move=> wo bo oi.
by rewrite (ordinal_o_isu1 wo (ordinal_o_wor bo) oi) (ordinal_o_o bo).
Qed.
Lemma worder_invariance r r':
r \Is r' -> worder r -> worder r'.
Proof.
move=> [f [or or' [bf sf tf] sif]] [_ wor].
split =>//.
move=> x xsr [y yx].
set A := image_by_fun (inverse_fun f) x.
move: (inverse_bij_fb bf) => bif.
have fi: function (inverse_fun f) by fct_tac.
have sxt: (sub x (target f)) by rewrite tf.
have sxs: (sub x (source (inverse_fun f))) by aw.
have sx :source f = (target (inverse_fun f)) by aw.
have Asx: sub A (substrate r).
rewrite - sf sx; apply: sub_trans (fun_image_Starget fi).
by apply: dirim_S.
have neA: (nonempty A) .
exists (Vf (inverse_fun f) y); apply /(Vf_image_P fi sxs); ex_tac.
move: (wor _ Asx neA) => [z []]; aw.
move=> zA zle; move: (zA) => /(Vf_image_P fi sxs) [u ux Wu].
have utx: (inc u (target f)) by apply: sxt.
move: (inverse_V bf utx) => uW.
exists u; red; aw; split =>// v vx; apply /iorder_gleP => //.
have vt: (inc v (target f)) by apply: sxt.
set v':= Vf (inverse_fun f) v.
have vA: inc v' A by apply /(Vf_image_P fi sxs); ex_tac.
rewrite - (inverse_V bf vt) - uW - sif.
- rewrite -Wu; move: (iorder_gle1 (zle _ vA)); aw.
- rewrite sx; fprops.
- rewrite sx; fprops.
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.
move: (OS_ordinal wor) => ox.
move: (ordinal_o_wor ox) => wor2.
move: (order_isomorphism_w is1) => m1.
move: (order_isomorphism_w is2) => m2.
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:= image_by_fun 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.
move: injf=> [_ bi2]; apply: bi2 => //.
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.
red; 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); rewrite /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 red; aw.
red; 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); rewrite /ordinal_leD1.
by split => //; move => [_ _].
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); exists w; split => //.
apply: (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; move => [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 => //.
move: (order_morphism_fi om) => injf.
move: om => [o1 o2 [ff sf tf] mf].
exists f; split => //; split => //.
split => //;apply: surjective_pr4; [fct_tac |rewrite tf v //].
move=> [t xsr rgf].
split => //; exists f; exists t; split => //.
by rewrite - (ordinal_o_sr x').
move=> [or or' [f [t [xsr rgf om]]]].
move: (ordinal_o_wor or') => wodr.
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.
move:(iorder_osr oc Xs)=> [or1 sr1].
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.
red; 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 _].
red; rewrite ordinal_o_sr //; split; fprops.
exists (identity x); exists x; split => //.
have ->: induced_order (ordinal_o y) x = (ordinal_o x).
rewrite /ordinal_o/induced_order/ordinal_o/graph_on.
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 by ord_tac0.
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.
Notation "x <=o y" := (ordinal_le x y) (at level 60).
Notation "x <o y" := (ordinal_lt x y) (at level 60).
Lemma ord_leP a: ordinalp a ->
forall x, (x <=o a <-> inc x (succ_o 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 ord_ltP0 x y:
x <o y <-> [/\ 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 ord_ltP a: ordinalp a -> forall x, (x <o a <-> inc x a).
Proof.
move=> oa x; split; first by move/ord_ltP0 => [_].
move => xa; apply/ord_ltP0; split => //; ord_tac0.
Qed.
Theorem wordering_ordinal_le: 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 _].
set y := (intersection x).
have yx:inc y x by apply: ordinal_setI.
exists y.
red; rewrite (graph_on_sr ale); split=> // a ax.
move: (alo _ ax) (alo _ yx) => Ka Ky.
by apply /graph_on_P1;split => //; split => //; apply: setI_s1.
Qed.
Lemma wordering_ordinal_le_pr x:
ordinal_set x -> worder_on (graph_on ordinal_le x) x.
Proof.
move => osx.
apply: wordering_pr; first by apply: wordering_ordinal_le.
by move => a /osx ox; split.
Qed.
Lemma ordinal_le_order_r: order_r ordinal_le.
Proof. by move: wordering_ordinal_le => [h1 _]. 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 (substrate x) (substrate x) by [].
move: (iorder_osr ox ss) => [pa pb].
split => //;hnf;rewrite /bijection_prop identity_s identity_t pb.
split => //; first by split => //;apply: identity_fb.
red; aw; move=> z y xsr ysr; bw.
symmetry; exact:(iorder_gleP x xsr ysr).
Qed.
Lemma ord_leR x: ordinalp x -> x <=o x.
Proof. move=> or; split => //. Qed.
Lemma ord_leT x y z: x <=o y -> y <=o z -> x <=o z.
Proof. move: ordinal_le_order_r => [p1 p2 _]; apply: p1. Qed.
Lemma ord_leA x y: x <=o y -> y <=o x -> x = y.
Proof. move: ordinal_le_order_r => [p1 p2 _]; apply: p2. Qed.
Lemma ord_leA1 a b: a <=o b -> b <o a -> False.
Proof. by move=> ole [olt one]; case: one; apply: ord_leA. Qed.
Lemma ord_lt_leT a b c: a <o b -> b <=o c -> a <o c.
Proof.
move=> [ab nab] bc; split; first by apply: (ord_leT ab bc).
by dneg ac; rewrite -ac in bc; apply: ord_leA.
Qed.
Lemma ord_le_ltT a b c: a <=o b -> b <o c -> a <o c.
Proof.
move=> ab [bc nbc]; split; first by apply: (ord_leT ab bc).
by dneg ca; rewrite ca in ab; apply: ord_leA.
Qed.
Lemma ord_lt_ltT a b c: a <o b -> b <o c -> a <o c.
Proof. by move=> [ab _] bc; apply: (ord_le_ltT ab bc). Qed.
Lemma ord_le_to_el a b:
ordinalp a -> ordinalp b ->
a <=o b \/ b <o a.
Proof.
move=> oa ob.
case: (ordinal_trichotomy oa ob).
- move => h; move: (ordinal_sub2 ob h) => [pa pb]; left; split => //.
- by right; apply/ord_ltP0.
- by move=> ->; left; apply:ord_leR.
Qed.
Lemma ord_le_to_ell a b:
ordinalp a -> ordinalp b ->
[\/ a = b, a <o b | b <o a].
Proof.
move=> oa ob.
case: (ord_le_to_el oa ob) => h;case: (equal_or_not a b) => ab; in_TP4.
Qed.
Lemma ord_le_to_ee a b:
ordinalp a -> ordinalp b -> a <=o b \/ b <=o a.
Proof.
by move=> oa ob; case: (ord_le_to_el oa ob); [by left | move => [h _]; right ].
Qed.
Lemma ord_le_to_si a b:
ordinalp a -> ordinalp b -> (sub a b \/ inc b a).
Proof.
move=> oa ob; case: (ord_le_to_el oa ob); first by move => [_ _]; left.
by move/ord_ltP0 => [_ _]; right.
Qed.
Ltac ord_tac :=
match goal with
| h: _ <=o ?x |- ordinalp ?x
=> move: h => [_ h _]; exact h
| h: ?x <=o _ |- ordinalp ?x
=> move: h => [h _ _]; exact h
| h: _ <o ?x |- ordinalp ?x
=> move: h => [[_ h _] _]; exact h
| h: ?x <o _ |- ordinalp ?x
=> move: h => [[h _ _] _]; exact h
| h1: ?x <=o ?y, h2: ?y <=o ?x |- ?x = ?y
=> apply: (ord_leA h1 h2)
| h1: ?x <=o ?y, h2: ?y <=o ?z |- ?x <=o ?z
=> apply: (ord_leT h1 h2)
| h1: ?x <o ?y, h2: ?y <=o ?z |- ?x <o ?z
=> apply: (ord_lt_leT h1 h2)
| h1: ?x <=o ?y, h2: ?y <o ?z |- ?x <o ?z
=> apply: (ord_le_ltT h1 h2)
| h1: ?x <o ?y, h2: ?y <o ?z |- ?x <o ?z
=> apply: (ord_lt_ltT h1 h2)
| h1: ?x <=o ?y, h2: ?y <o ?x |- _
=> case: (ord_leA1 h1 h2)
| h1: ordinalp ?x, h2: inc ?y ?x |- ordinalp ?y
=> apply: (ordinal_hi h1 h2)
| h1: ordinalp ?x |- ?x <=o ?x
=> apply: (ord_leR h1)
| h1: ?x <o ?y |- ?x <=o ?y
=> by move: h1 => []
| h1: ordinalp ?a, h2: inc ?x ?a |- ?x <o ?a =>
by apply/(ord_ltP h1)
| h2: ?x <o ?a |- inc ?x ?a =>
by move/ord_ltP0: h2 => [_ _]
| h1: ordinalp ?a, h2: inc ?x ?a |- ?x <=o ?a =>
by move: h2 => /(ord_ltP h1) []
| h1: ?x = succ_o ?y |- inc ?y ?x => by rewrite h1; fprops
end.
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: (or) => [gr _ _ _]; move: (gr _ tr) => p; rewrite -p.
by apply: h; hnf; rewrite p.
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).
move: (iorder_osr o2 aa) => [sa sb].
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.
move: (order_cp1 wo1 wo2 xy) => [pa pb].
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 <o ordinal y.
Proof.
move => 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 => //; move=> t ot pt;move: (p3 _ ot pt) => zt; red;split => //.
Qed.
Lemma least_ordinal2 (p: property) x:
(forall y, ordinalp y -> (forall z, z <o y -> 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.
ex_middle bad; move:(p3 _ (proj31_1 zx) bad) => le; ord_tac.
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 <o y -> p z)].
Proof.
move=> ox px.
move: (least_ordinal4 (p:= (fun z => ~ p z)) ox px) => [p1 p2 p3].
split => //; move=> z zy.
have oz: ordinalp z by ord_tac.
ex_middle npz; move: (p3 _ oz npz) => lt; ord_tac.
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 => //.
move => z /(ord_ltP pa); apply: pc.
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).
Notation "\opred" := union (only parsing).
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].
apply: (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: ordinal_set E ->
ordinalp y -> ordinal_ub E y ->
(\osup E) <=o y.
Proof.
move=> /OS_sup Ep oy h; split => //.
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); rewrite /p; split => //; move => y; split.
move => h.
have oy: ordinalp y by ord_tac.
split => //; move=> i iE; exact (ord_leT (ord_sup_ub alo iE) h).
by move=> [oy aly]; apply: ord_ub_sup.
have p1: forall x, p x -> ordinal_ub E x.
rewrite /p; move=> t [ox Ex].
have : t <=o t by ord_tac.
by rewrite (Ex t); move => [_].
have p2: forall x y, p x -> ordinalp y ->
(ordinal_ub E y) -> x <=o y.
rewrite /p; move=> x1 y1 [ox opf] oy h; rewrite opf; split => //.
move=> x y fx fy.
have ox: ordinalp x by move: fx => [ox _ ].
have oy: ordinalp y by move: fy => [oy _ ].
move: (p2 _ _ fy ox (p1 _ fx)) (p2 _ _ fx oy (p1 _ fy))=> h1 h2.
ord_tac.
Qed.
The empty set is the least ordinal
Definition ord_zero := emptyset.
Notation "\0o" := ord_zero.
Lemma OS0: ordinalp \0o.
Proof. move => y ye _ yne; case: yne; 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 <o x.
Proof. by move => ox xnz; split; [ apply: ozero_least | apply nesym ]. Qed.
Lemma ord_le0 x: x <=o \0o -> x = \0o.
Proof. move/(ord_leP OS0) => /setU1_P; case => //; case; case. Qed.
Lemma ord_ne_pos x: ordinalp x -> nonempty x -> \0o <o x.
Proof. by move=> ox /nonemptyP nex; apply:ord_ne0_pos. Qed.
Lemma ord_ne_has0 x: ordinalp x -> x <> \0o -> inc \0o x.
Proof.
move=> ox xnz.
by case: (ordinal_sub OS0 ox (sub0_set x)) => // eqz; case: xnz.
Qed.
Lemma ord_lt0 x: x <o \0o -> False.
Proof. by move=> [pa pab]; move: (ord_le0 pa). Qed.
Lemma ord_gt_ne0 x y: x <o y -> y <> \0o.
Proof. move => xy yz; rewrite yz in xy; exact: (ord_lt0 xy). Qed.
succ_o x is the next ordinal after x
Lemma osucc_pr x (z:= succ_o x): ordinalp x ->
x <o z /\ (forall w, x <o w -> z <=o w).
Proof.
move=> ox; move: (OS_succ ox)=> oy.
split; first by apply/ord_ltP0; split => //; rewrite /z; fprops.
move=> w /ord_ltP0 [_ ow xw].
split => //; move=> t /setU1_P;case; last by move=> ->.
by apply: (ordinal_transitive ow).
Qed.
Lemma ord_succ_lt a: ordinalp a -> a <o (succ_o a).
Proof. move=> oa; apply /ord_ltP0; split;fprops. Qed.
Lemma ord_lt_succP a b: a <o (succ_o b) <-> a <=o b.
Proof.
split.
move /ord_ltP0=> [p1 /OS_succr p2 p3].
by split => //; apply: ordinal_sub3.
move => [p1 p2]; move/(ordinal_sub4P p1 p2) => q; apply/ord_ltP0.
split; fprops.
Qed.
Lemma ord_succ_ltP a b: a <o b <-> (succ_o 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 /ord_ltP0;split => //; ord_tac.
Qed.
Lemma ord_le_succ_succP x y: x <=o y <-> (succ_o x <=o succ_o y).
Proof.
split => h; first by apply /ord_succ_ltP /ord_lt_succP.
by apply /ord_lt_succP /ord_succ_ltP.
Qed.
Lemma ord_lt_succ_succP x y: (x <o y) <-> (succ_o x <o succ_o y).
Proof.
split => h; first by apply /ord_lt_succP /ord_succ_ltP.
by apply /ord_succ_ltP /ord_lt_succP.
Qed.
Definition succ_op x := exists2 y, ordinalp y & x = succ_o y.
Lemma succ_op_pr a: ordinalp a -> (exists b, a = succ_o b) ->
exists2 b, ordinalp b & a = succ_o b.
Proof. by move => oa [b bs]; exists b=> //; apply: OS_succr; rewrite - bs. Qed.
Lemma osuccVidpred x: ordinalp x ->
exactly_one (succ_op x) (x = \opred x).
Proof.
move=> ox.
case: (equal_or_not x (union x)) => h.
split; [by right | move=> [[y oy yt] _] ].
have: inc y x by rewrite yt; fprops.
rewrite h => /setU_P [a ya]; rewrite yt => ay.
move/(ord_ltP (OS_succ oy)): ay => /ord_lt_succP ay1.
exact: (ordinal_irreflexive oy (proj33 ay1 _ ya)).
split; [left; apply:succ_op_pr => // | by case].
have p1: sub (union x) x by move=> t /setU_P [y ty yx]; ord_tac0.
move: (setC_ne (conj p1 (nesym h))) => [y /setC_P [yx yp]].
have p3: sub (succ_o y) x.
move =>t /setU1_P; case; [ move => ty;ord_tac0 | by move=> ->].
have oy:=(OS_succ (ordinal_hi ox yx)).
exists y; apply: ord_leA; split => // t tx; apply /setU1_P.
case: (ordinal_trichotomy (ordinal_hi ox yx)(ordinal_hi ox tx)); fprops.
by move => yt; move: (setU_i yt tx).
Qed.
a limit ordinal is a non-successorr; it contains zero and is stable
by succ_o; 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 (succ_o y) x)].
Lemma limit_ordinal_P1 x: ordinalp x ->
((limit_ordinal x) <-> (nonempty x /\ x = union x)).
Proof.
move=> ox.
move: (ordinal_irreflexive ox) => ir.
split.
move=> [_ nex p]; split; first by exists emptyset.
case: (proj1 (osuccVidpred ox)) => // [] [y oy xy].
have yx: (inc y x) by ord_tac.
by move: (p _ yx); rewrite -xy => bad.
move=> [nex xu]; split=>//.
by move: (ord_ne_pos ox nex)=> h; ord_tac.
move=> y yx; move: (ordinal_hi ox yx)=> oy.
case: (ordinal_trichotomy (OS_succ oy) ox) =>//.
case /setU1_P => h; last by rewrite -h in yx.
by move:((ordinal_transitive ox yx) _ h).
move: (osuccVidpred ox)=> [ _ dj] h.
case: dj; split => //; by exists y.
Qed.
Lemma limit_ordinal_pr2 x: ordinalp x ->
[\/ x = \0o, succ_op x | limit_ordinal x].
Proof.
move=> ox.
case: (emptyset_dichot x); first by constructor 1.
move=> nex.
move: (osuccVidpred ox) => [h _]; case: h; first by constructor 2.
by move=> xu; constructor 3; apply /(limit_ordinal_P1 ox).
Qed.
Lemma limit_ordinal_P3 x:
limit_ordinal x <->
(\0o <o x /\ forall t, t <o x -> succ_o t <o x).
Proof.
split.
move => [ox xnz xl]; split.
+ by apply: (ord_ne0_pos ox) => xz; move: xnz; rewrite xz; move/in_set0.
+ by move => t /(ord_ltP ox) => h; apply/(ord_ltP ox); apply: xl.
move => [[[_ ox sa] xnz] sb]; split => //.
+ apply: ord_ne_has0; fprops.
+ by move => t /(ord_ltP ox) => h; apply/(ord_ltP ox); apply: sb.
Qed.
Lemma succo_K y: ordinalp y -> \opred (succ_o 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; ord_tac0.
Qed.
Lemma predo_K x: ordinalp x -> succ_op x -> succ_o (\opred x) = x.
Proof.
by move=> ox [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].
set g := Lf (fun z => Yo (z = a') (Vf f a) (Vf f z)) x y.
exists g; rewrite /g;split => //; aw.
have xsf: inc a (source f) by rewrite sf; fprops.
have sxsf: sub x (source f) by rewrite sf; move=> t; fprops.
apply: lf_bijective.
move=> z bx; simpl; 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.
rewrite -aux in vx; contradiction.
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 => //.
move=> ax;move: zt; rewrite zW -{1} ax Wa => nyy; contradiction.
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 aux.
have nbx: ~ inc b x by dneg bx; apply: sxy.
move: (equipotentS aux)=> [f [[[ff injf] sjf] sf tf]].
eqsym; clear aux.
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.
move=> h; rewrite -(injf _ _ Asf vsf h) in vx; contradiction.
case:aux => vy => //.
move: (Byp _ vy) => aux;Ytac0 => h; rewrite -h in vx; contradiction.
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 => //.
move=> 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 otehrwise; note that ordinalp x is missing in the definition
of infinite
Definition infinite_o u := u \Eq (succ_o u).
Definition finite_o u := ordinalp u /\ ~ (infinite_o u).
Lemma infinite_o_increasing x y: ordinalp x -> ordinalp y ->
inc x y -> infinite_o x -> infinite_o y.
Proof.
rewrite /infinite_o; move=> ox oy xy.
apply: setU1_injective_card1 (ordinal_irreflexive ox)
(ordinal_irreflexive oy) (ordinal_transitive oy xy).
Qed.
Lemma finite_o_increasing x y: inc x y -> finite_o y -> finite_o x.
Proof.
move=> xy [oy niy].
have ox: ordinalp x by ord_tac0.
by split => //; dneg nix; apply: (infinite_o_increasing ox oy xy).
Qed.
Lemma succ_injective_oP x y: ordinalp x -> ordinalp y ->
((succ_o x) \Eq (succ_o 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 (succ_o x) <-> infinite_o x).
Proof. move=> ox; apply/ (succ_injective_oP ox (OS_succ ox)). Qed.
Lemma finite_oP x: finite_o (succ_o x) <-> finite_o x.
Proof.
split.
move=> [p1 p2].
have ox: ordinalp x by apply: OS_succr.
by move: p2 => /(infinite_oP ox) => h; split.
by move=> [p1 p2]; split; [ apply: OS_succ | move/(infinite_oP p1)].
Qed.
limit ordinals are infinite, since succ_o is a bijecion for
the least infinite ordinal
Lemma limit_infinite 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: (infinite_o_increasing oA ox Ax p).
move: (ordinal_irreflexive oA) => nAA.
pose f z := Yo (inc z A) (succ_o z) emptyset.
eqsym;exists (Lf f (succ_o A) A); split => //; aw.
have q1: forall z, inc z (succ_o 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.
- move=> eq.
have:inc u (succ_o u) by fprops.
have:inc v (succ_o v) by fprops.
rewrite eq - {1} eq;case /setU1_P => // uv; case /setU1_P => // vu.
case: (ordinal_asymmetric oA uA vA vu uv).
- move=> bad; empty_tac1 u.
- move=> bad; symmetry in bad; empty_tac1 v.
- done.
set z':= Zo A (fun z=> ~ (exists2 x0, inc x0 (succ_o A)& z = f x0)).
case: (emptyset_dichot z') => nez.
move=> y yA; ex_middle bad;empty_tac1 y; apply: Zo_i => //.
have alo': ordinal_set z' by move => a /Zo_P [aA _]; ord_tac.
move: (ordinal_setI nez alo').
set B:= intersection z';move => iz'.
move: (iz') => /Zo_P [r1 r2].
move: (ordinal_hi oA r1) => oB.
case: (emptyset_dichot B) => be.
by case: r2; exists A => //; fprops; rewrite /f Y_false.
suff aux: (limit_ordinal B).
move: ((leA _ oB aux) _ r1) => sab.
by case: (ordinal_irreflexive oB).
apply/(limit_ordinal_P1 oB); split =>//.
move: (osuccVidpred oB) => [ca _ ]; case: ca =>//; move=> [y oy ta].
have yB: inc y B by rewrite ta; fprops.
have yA: inc y A by apply: (ordinal_transitive oA r1 yB).
have yAA: inc y (succ_o A) by rewrite /succ_o;fprops.
have fy: f y = B by rewrite ta /f; Ytac0.
case: r2; ex_tac.
Qed.
The cardinal of x is the least ordinal equipotent to x
Definition cardinalV x :=
(least_ordinal (equipotent x) (ordinal (worder_of x))).
Definition cardinalV_prop x y :=
[/\ ordinalp y, x \Eq y &
(forall z, ordinalp z -> x \Eq z -> sub y z)].
Lemma cardinalV_unique x y z:
cardinalV_prop x y -> cardinalV_prop x z -> y = z.
Proof.
move=> [By exy p1] [Bz exz p2].
by apply: extensionality; [ apply: p1 | apply: p2 ].
Qed.
Lemma cardinalV_pr0 x: cardinalV_prop x (cardinalV x).
Proof.
move: (Zermelo_ter x)=> [wor sr].
move: (ordinal_isomorphism_exists wor) => [or oi].
set f :=(ordinal_iso (worder_of x)) in or oi.
have extf: x \Eq (ordinal (worder_of x)).
move : oi => [_ _ [bf sf tf] ff]; exists f; first by split => //; ue.
apply: (least_ordinal1 or extf).
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.
Lemma card_card x: cardinalp x -> cardinal x = x.
Proof.
move=> [cx1 cx2].
have aux: cardinalV_prop x (cardinal x) by apply: cardinalV_pr.
have aux': cardinalV_prop x x by split; fprops.
apply: (cardinalV_unique aux aux').
Qed.
Ltac eq_aux:= match goal with
H: cardinalp ?a |- cardinal ?b = ?a => rewrite- (card_card H); aw
| H: cardinalp ?a |- ?a = cardinal ?b => rewrite- (card_card H); aw
end.
Lemma CS_cardinal x: cardinalp (cardinal x).
Proof.
move: (cardinalV_pr x) => [p1 p2 p3].
split => //; move=> z Bz ez; apply: p3 => //; eqtrans (cardinal x).
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 (cardinalV_pr x)). Qed.
Lemma cardinal_pr x: (cardinal x) \Eq x.
Proof. by eqsym; apply: cardinal_pr0. Qed.
Lemma cardinal_ordinal_le x: ordinalp x -> cardinal x <=o x.
Proof.
move => ox.
move: (cardinalV_pr 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.
split => h.
eqtrans (cardinal x); rewrite h; eqsym; fprops.
move: (cardinalV_pr x) (cardinalV_pr y) => [Bx exo lx][By eyp ly].
apply: extensionality.
apply: lx =>//; eqtrans y.
by apply: ly =>//; eqtrans x; eqsym.
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 (image_by_fun f x) = cardinal x.
Proof. by move => pa /(equipotent_restriction1 pa)/card_eqP. Qed.
Lemma cardinal_range f: injection f ->
cardinal (range (graph f)) = (cardinal (source f)).
Proof. by move /equipotent_range /card_eqP. Qed.
Lemma cardinal_indexed a b: cardinal (a *s1 b) = cardinal a.
Proof. symmetry;apply /card_eqP; apply:equipotent_indexed. Qed.
Lemma cardinal_indexedr a b: cardinal (indexedr b a) = cardinal a.
Proof. symmetry;apply /card_eqP; apply:equipotent_rindexed. Qed.
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 succ_o_zero: succ_o \0o = \1o.
Proof.
set_extens z.
move/setU1_P; case; [ case; case | move => ->//; apply:set1_1].
move /set1_P => ->; fprops.
Qed.
Lemma succ_o_one: succ_o \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.
Lemma constants_v: (C0 = \0c /\ C1 = \1c /\ C2 = \2c).
Proof. by []. Qed.
Lemma OS1: ordinalp \1o.
Proof. rewrite - succ_o_zero; apply: OS_succ; apply: OS0. Qed.
Lemma OS2: ordinalp \2o.
Proof. rewrite - succ_o_one; apply: OS_succ; apply: OS1. Qed.
Lemma equipotent_to_emptyset x: x \Eq emptyset -> x = emptyset.
Proof.
move=> [y [[[fy _] suy] sy ty]].
apply /set0_P => z zx; empty_tac1 (Vf y z); Wtac.
Qed.
Lemma cardinal_set0: cardinal emptyset = \0c.
Proof. apply: equipotent_to_emptyset; apply: (cardinal_pr emptyset). Qed.
Lemma cardinal_nonemptyset x:
cardinal x = \0c -> x = emptyset.
Proof.
rewrite - cardinal_set0; move /card_eqP.
apply: equipotent_to_emptyset.
Qed.
Lemma cardinal_nonemptyset0 x: x <> \0c -> cardinal x <> \0c.
Proof. by move => pa pb; case: pa; apply: cardinal_nonemptyset. Qed.
Lemma cardinal_nonemptyset1 x:
nonempty x -> cardinal x <> \0c.
Proof. by move=> nex; apply :cardinal_nonemptyset0; apply /nonemptyP. Qed.
Lemma card1_nz: \1c <> \0c.
Proof. exact: TP_ne1. Qed.
Lemma card2_nz: \2c <> \0c.
Proof. exact: (proj1 C2_neC01). Qed.
Lemma card_12: \1c <> \2c.
Proof. exact: (nesym (proj2 C2_neC01)). 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: (equipotentS h); rewrite /card_zero=> h'.
move: (equipotent_to_emptyset h') => h''.
have [[]]: inc \0o emptyset by rewrite - h'' /succ_o; fprops.
Qed.
Lemma finite_one: finite_o \1o.
Proof. rewrite - succ_o_zero; apply /finite_oP; apply:finite_zero. Qed.
Lemma finite_two: finite_o \2o.
Proof. by rewrite - succ_o_one; apply /finite_oP; apply:finite_one. Qed.
Lemma finite_succ x:
finite_o x <-> (x = emptyset \/ (exists2 y, finite_o y & x = succ_o y)).
Proof.
split.
move => fx; move: (fx) => [ox nix].
case: (limit_ordinal_pr2 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: (limit_infinite h).
case; first by move => ->; apply: finite_zero.
by move=> [y fy ->];apply/finite_oP.
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 rewrite /A; 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; rewrite /D=> t tD; apply: (setI_hi tD xC).
have DA: inc D A.
rewrite /A; apply: Zo_i.
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.
have TC: (inc T C) by apply: Zo_i.
by move: ((p1 _ TC) _ 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 [if1 sf1 tf1]][f2 [if2 sf2 tf2]].
set Z := image_by_fun f2 Y.
have e1: Y \Eq Z by apply: equipotent_restriction1 => //; rewrite sf2; fprops.
suff e2: X \Eq Z.
have //: X \Eq Y by eqtrans Z; eqsym.
set g:= fun w => Vf (Vf w f1) f2.
have ff2: function f2 by fct_tac.
have ff1: function f1 by fct_tac.
move: (f_range_graph ff2) => rg2.
move: (image_by_fun_source ff2); rewrite /image_of_fun sf2 -/Z => zv.
apply: (Cantor_Bernstein1).
- rewrite zv -tf2; apply f_range_graph; fct_tac.
- 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.
move: if1 => [_ prop]; apply: prop => //.
move: if2 => [_ prop2].
apply: prop2 => //;rewrite sf2 -tf1;Wtac.
Qed.
a finite ordinal is a cardinal ; so zero, one and two are cardinals
Lemma CS_succ_o x: finite_o x -> cardinalp (succ_o x).
Proof.
move=> [ox nix]; apply/cardinalP; split; first by apply: OS_succ.
move=> z zo.
dneg aux1; eqtrans z; last by eqsym.
have zx: (sub z x).
move: zo;case /setU1_P; [apply: (ordinal_transitive ox) | move=> ->; fprops].
move: (ordinal_irreflexive ox) => xx.
move: aux1 => [g [[[fg injg] sjg] sg tg]].
pose f z := Vf g z.
have p1: (forall t, inc t x -> inc (f t) z).
by rewrite -tg /f=>t tx; Wtac; rewrite sg; apply: setU1_r.
have p2:(forall u v, inc u x -> inc v x -> f u = f v -> u = v).
by rewrite /f => u v uE vE; apply: injg; rewrite sg ;apply: setU1_r.
apply: (Cantor_Bernstein1 zx p1 p2).
Qed.
Lemma CS0: cardinalp \0c.
Proof.
apply/cardinalP; split; [by apply: OS0 | move=> z;case; case].
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_succ_o.
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_pr1 y z: infinite_c z ->
z = succ_o y -> False.
Proof.
move => [] /cardinalP [c1 c2] iz zyy.
rewrite zyy in c1 c2 iz.
have yz: (inc y (succ_o y)) by fprops.
move: (ordinal_hi c1 yz) => /(infinite_oP) h; move /h: iz => io.
by case: (c2 _ yz); eqsym.
Qed.
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.
We define here the cardinal successor
Definition succ x := cardinal (succ_o x).
Lemma CS_succ a: cardinalp (succ a).
Proof. rewrite /succ; fprops. Qed.
Lemma cardinal_irreflexive x: cardinalp x -> ~ (inc x x).
Proof. move=> [ox _]; apply: (ordinal_irreflexive ox). Qed.
Theorem succ_injective1: {when cardinalp &, injective succ}.
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 card_succ_pr a b: ~ (inc b a) ->
cardinal (a +s1 b) = succ (cardinal a).
Proof.
move=> bna; apply /card_eqP.
apply /setU1_injective_card2 => //;last by fprops.
apply: cardinal_irreflexive; fprops.
Qed.
Lemma card_succ_pr1 a b:
cardinal ((a -s1 b) +s1 b) = succ (cardinal (a -s1 b)).
Proof. rewrite card_succ_pr //; apply: setC1_1. Qed.
Lemma card_succ_pr2 a b: inc b a ->
cardinal a = succ (cardinal (a -s1 b)).
Proof. move=> ba; rewrite - {1} (setC1_K ba); apply: card_succ_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: (card_succ_pr2 ba); rewrite -eq /succ //.
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/succ_o => eq1 eq2.
set (a:= (x +s1 x)).
move: (equipotentS eq1) => eq3.
have eq : a -s1 x = x by apply: setU1_K.
rewrite - eq; apply: infinite_set_pr1 ; [ rewrite /a; 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.
apply: (infinite_set_pr zn).
set f:= triple nat (nat -s1 (Ro 0)) (gacreate S).
have gf: graph f = (gacreate S) by rewrite /f; aw.
have p0: fgraph (gacreate S).
split.
move=> t /IM_P [a <-]; fprops.
move=> x y /IM_P [a <-] /IM_P [b <-]; aw => sp.
by rewrite sp (R_inj sp).
have p1: sgraph (gacreate S) by fprops.
have p2:nat = domain (gacreate S).
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 (gacreate S))= (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).
have [w wp]: exists w:nat, t = Ro w by exists (Bo tn); rewrite (B_eq tn).
have: w <> 0 by dneg xx; ue.
rewrite wp;clear to wp.
case: w => // n _; exists (Ro n); apply/IM_P; exists n =>//.
have ff: function f.
apply: function_pr =>//; rewrite p3; fprops.
have sf: surjection f by apply: surjective_pr4 =>//;rewrite /f; aw.
exists f; rewrite /f;red;aw; split => //; split => //.
apply: injective_pr_bis =>//.
move=> x x' y; rewrite /related gf => /IM_P [a J1] /IM_P [b J2].
move: (pr2_def J1)(pr2_def J2)=> r3 r4.
rewrite -r4 in r3; move: (R_inj r3)=> r5.
by rewrite -(pr1_def J1) - (pr1_def J2) (eq_add_S _ _ r5).
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. by move: omega0_pr => [h _ ]. Qed.
Hint Resolve OS0 OS1 OS2 OS_omega : fprops.
Lemma omega_infinite: infinite_o omega0.
Proof. by move: omega0_pr => [_ h _]. Qed.
Lemma omega_P1 x: ordinalp x ->
(infinite_o x <-> sub omega0 x).
Proof.
move=> ox; split; first by move: omega0_pr => [_ _ h]; apply: h.
move: omega_infinite OS_omega => bi oo sox.
case: (ordinal_sub oo ox sox); first by move => <- //.
move=> h; apply: (infinite_o_increasing oo ox h bi).
Qed.
Lemma omega_P2 x: inc x omega0 <-> finite_o x.
Proof.
move: OS_omega => oo.
split => xo.
have ox:= (ordinal_hi oo xo).
split=>//; move /(omega_P1 ox) => h.
case: (ordinal_irreflexive ox (h _ xo)).
move: xo => [ox nifx].
by case:(ord_le_to_si oo ox) => // /(omega_P1 ox).
Qed.
Lemma CS_omega: cardinalp omega0.
Proof.
move: OS_omega => oo;split => // => z oz pa; apply /(omega_P1 oz).
move: omega_infinite => h.
eqtrans (succ_o omega0); first by eqtrans omega0; eqsym.
by apply /succ_injective_oP.
Qed.
Lemma omega_infinitec: infinite_c omega0.
Proof. split; [ apply: CS_omega | apply: omega_infinite]. Qed.
Lemma omega_limit0: omega0 = \opred omega0.
Proof.
case (proj1 (osuccVidpred OS_omega)) =>//.
move=> [y oy ys].
have : inc y omega0 by rewrite ys ; fprops.
move => /omega_P2 /finite_oP; rewrite -ys; move => [_[]].
apply: omega_infinite.
Qed.
Lemma omega_limit: limit_ordinal omega0.
Proof.
apply/(limit_ordinal_P1 OS_omega).
split; last by apply: omega_limit0.
exists \0c; apply /omega_P2; apply: finite_zero.
Qed.
Lemma omega_limit2 x: limit_ordinal x -> omega0 <=o x.
Proof.
move=> h; move: (h) => [Bx _]; split; fprops.
apply/(omega_P1 Bx); apply: (limit_infinite h).
Qed.
Some properties of infinite sets
Lemma infinite_card_limit1 x: infinite_c x -> \opred x = x.
Proof.
move => icx.
move: (osuccVidpred (OS_cardinal (proj1 icx))) => [p3 _].
case: p3 => // [] [y _ h]; case: (infinite_pr1 icx h).
Qed.
Lemma infinite_card_limit2 x: infinite_c x -> limit_ordinal x.
Proof.
move => ic; move: (ic) => [p1 p2].
apply /(limit_ordinal_P1 (OS_cardinal p1)).
split; last by symmetry;apply: infinite_card_limit1.
by case: (emptyset_dichot x) => // xe; case: (infinite_nz ic).
Qed.
Lemma omega_limit3 x: infinite_c x -> sub omega0 x.
Proof.
by move=> h; move: (omega_limit2 (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.
Lemma set1_equipotent x y:
singleton x \Eq singleton y.
Proof.
move: (set1_order_is x y) => [f [_ _ [pa pb pc] _]].
move: pb pc;rewrite (proj2 (set1_wor x)) (proj2 (set1_wor y)) => <- <-.
by exists f.
Qed.
Lemma cardinal_set1 x: cardinal (singleton x) = \1c.
Proof. rewrite -(card_card CS1); apply /card_eqP; apply: set1_equipotent. Qed.
Lemma set2_equipotent1 x y: x <> y ->
exists g, [/\ bijection_prop g (doubleton x y) C2,
Vf g x = C0 & Vf g y = C1].
Proof.
move => neq.
have ax: lf_axiom (fun z => Yo (z = x) C0 C1) (doubleton x y) C2.
by move => t tp; apply /set2_P; Ytac h; [left | right].
exists (Lf (fun z => Yo (z = x) C0 C1 ) (doubleton x y) C2).
split; aw; fprops; try Ytac0 =>//.
split; aw;apply: lf_bijective.
done.
move=> u v /set2_P [] -> /set2_P [] ->; Ytac0 => //; Ytac0 => // => h.
by case: TP_ne.
by case: TP_ne1.
by move => z; case/C2_P => ->; [exists x | exists y]; fprops; Ytac0.
Qed.
Lemma set2_equipotent x y: x <> y -> doubleton x y \Eq \2c.
Proof. by move => /set2_equipotent1 [g [bg sg tg]]; exists g. Qed.
Lemma cardinal_set2 x x': x <> x' -> cardinal (doubleton x x') = \2c.
Proof.
move=> xx'; rewrite -(card_card CS2).
by apply /card_eqP /set2_equipotent.
Qed.
Lemma set_of_card_one x: cardinal x = \1c -> singletonp x.
Proof.
move=> xh; symmetry in xh; move: xh.
rewrite -(card_card CS1); move /card_eqP; rewrite /card_one.
move=> [f [[[ff injf] sf] srf tf]]; exists (Vf f emptyset).
rewrite -tf.
have p1: inc (Vf f emptyset) (target f) by Wtac; rewrite srf;fprops.
set_extens t; last by move /set1_P => ->.
move=> tx; move: ((proj2 sf) _ tx)=> [y]; rewrite srf.
move=> /set1_P -> <-; fprops.
Qed.
Lemma set_of_card_two x: cardinal x = \2c -> doubletonp x.
Proof.
move=> xh; symmetry in xh; move: xh.
rewrite -(card_card CS2); move /card_eqP; rewrite / card_two.
move=> [f [[[ff injf] sf] srf tf]].
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); exists (Vf f (singleton emptyset)); split.
by move=> aux; move: (injf _ _ es ses aux); fprops.
rewrite -tf; 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 equipotent_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).
red; 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 equipotent_setX a b a' b':
a \Eq a' -> b \Eq b' -> (a \times b) \Eq (a' \times b').
Proof.
rewrite !equipotentC.
move=> [f bf] [g bg]; exists (ext_to_prodC f g).
apply: (bijective_ext_to_prod2C bf bg).
Qed.
Hint Resolve equipotent_setX equipotent_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)).
exists (Lf g (a \times (b \times c)) ((a \times b) \times c)).
split => //; aw.
rewrite /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 aw;rewrite pPy py.
Qed.
Lemma distrib_union_prod2: right_distributive product union2.
Proof.
move => a b c;set_extens x.
move /setX_P => [pa pb] /setU2_P.
by case => pc; apply /setU2_P; [left | right]; apply:setX_i.
case /setU2_P => /setX_P [pa pb pc]; apply/setX_i => //; fprops.
Qed.
Lemma distrib_inter_prod2: right_distributive product intersection2.
Proof.
move => a b c;set_extens x.
by move/setX_P => [Px xa /setI2_P [pa pb]]; apply/setI2_P;split;apply/setX_P.
move /setI2_P => [] /setX_P [Px px qx1 /setX_P [_ _ qx2]].
apply/setX_P; split; fprops.
Qed.
Lemma equipotent_times_s1s1 a b c: (a *s1 b) \Eq (a *s1 c).
Proof. eqtrans a; eqsym; fprops. Qed.
Hint Resolve equipotent_times_s1s1: fprops.
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 red; 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].
red;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.
eqtrans (Vg X i); [by eqsym; fprops | eqtrans (Vg Y 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 =>//.
red;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_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: doubleton_fam f a b ->
let F := (variantLc a b) in
exists g, [/\ bijection g, target g = domain F &
f = F \cf (graph g)].
Proof.
move => [x [y [xy fgf df fx fy]]] F.
move: (set2_equipotent1 xy) => [g [[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.
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 (image_of_fun f).
rewrite -tgf; apply: fun_image_Starget; fct_tac.
exists (restriction_to_image f).
hnf;rewrite /restriction_to_image /restriction2; aw.
split => //;by apply: restriction_to_image_fb.
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=> eq1 [f [[injf _] sf tf]].
have [g [[injg _] sg tg]]: a' \Eq a by eqsym.
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 (equipotentS h1)(equipotentS 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 <c y" := (cardinal_lt x y) (at level 60).
Lemma ordinal_cardinal_le x y:
x <=c y -> 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: (ord_le_to_si ox oy) => // yx.
suff: (y \Eq z).
move=> eyz.
have : x \Eq y by eqtrans z; eqsym.
move /card_eqP.
rewrite (card_card cx) (card_card cy); move => -> //.
move: ezx => [f [[[f0 f1] _] f2 f3]].
have syx: (sub y x) by apply: (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 card_leR x: cardinalp x -> x <=c x.
Proof. by move=> cx;split. Qed.
Hint Resolve card_leR: fprops.
Lemma card_leT a b c:
a <=c b -> b <=c c -> a <=c c.
Proof.
rewrite/cardinal_le.
by move=> [ca cb eab] [_ cc ebc]; split => //; apply: sub_trans eab ebc.
Qed.
Lemma card_leA x y:
x <=c y -> y <=c x -> x = y.
Proof.
by move => [ca cb eab] [_ cc ebc]; apply: extensionality.
Qed.
Theorem cardinal_le_wor: worder_r cardinal_le.
Proof.
split => //.
split => //.
move=> a b c;apply: card_leT.
move=> a b; apply: card_leA.
move=> x y [cx cy _]; split; fprops.
move=> x xa [a ax].
have xc: cardinal_set x by move=> b bx; move: (xa _ bx)=> [ok _].
have xb: ordinal_set x by move=> b bx; move: (xa _ bx)=> [[ok _] _].
move: (least_ordinal1 (p:= fun w => (inc w x)) (xb _ ax) ax).
set y := least_ordinal (fun w => inc w x) a; move => [p1 p2 p3].
exists y; red; rewrite graph_on_sr //.
split => //; move=> u ux; apply graph_on_P1;split;fprops; split; fprops.
Qed.
The order on cardinals
Lemma not_card_le_lt a b: a <=c b -> b <c a -> False.
Proof. by move=> ab [ba nba]; case: nba; apply: card_leA.
Qed.
Lemma card_lt_leT a b c:
a <c b -> b <=c c -> a <c c.
Proof.
move=> [ab nab] bc; split.
apply: (card_leT ab bc).
by dneg ac; rewrite -ac in bc; apply: card_leA.
Qed.
Lemma card_le_ltT a b c:
a <=c b -> b <c c -> a <c c.
Proof.
move=> ab [bc nbc]; split.
apply: (card_leT ab bc).
by dneg ca; rewrite ca in ab; apply: card_leA.
Qed.
Lemma card_ltleA a b: a <c b -> ~(b <=c a).
Proof. move => h1 h2; exact: (not_card_le_lt h2 h1). Qed.
Lemma card_leltA a b: a <=c b -> ~(b <c a).
Proof. move => h1 h2; exact: (not_card_le_lt h1 h2). Qed.
Lemma card_lt_ltT a b c: a <c b -> b <c c -> a <c c.
Proof. move => h1 [h2 _]; exact: (card_lt_leT h1 h2). Qed.
Ltac co_tac := match goal with
| Ha: ?a <=c ?b, Hb: ?b <=c ?c |- ?a <=c ?c
=> apply: (card_leT Ha Hb)
| Ha: ?a <c ?b, Hb: ?b <=c ?c |- ?a <c ?c
=> apply: (card_lt_leT Ha Hb)
| Ha:?a <=c ?b, Hb: ?b <c ?c |- ?a <c ?c
=> apply: (card_le_ltT Ha Hb)
| Ha: ?a <c ?b, Hb: ?b <c ?c |- ?a <c ?c
=> induction Ha; co_tac
| Ha: ?a <=c ?b, Hb: ?b <c ?a |- _
=> case: (not_card_le_lt Ha Hb)
| Ha: ?x <=c ?y, Hb: ?y <=c ?x |- _
=> solve [ rewrite (card_leA Ha Hb) ; fprops ]
| Ha: ?a <=c _ |- cardinalp ?a => exact (proj31 Ha)
| Ha: _ <=c ?a |- cardinalp ?a => exact (proj32 Ha)
| Ha: ?a <c _ |- cardinalp ?a => exact (proj31_1 Ha)
| Ha: _ <c ?a |- cardinalp ?a => exact (proj32_1 Ha)
| Ha: ?a <c ?b |- ?a <=c ?b => by move: Ha => []
end.
Lemma wordering_cardinal_le_pr x:
cardinal_set x ->
(worder_on (graph_on cardinal_le x) x).
Proof.
move=> alc; apply: (wordering_pr cardinal_le_wor).
move=> a ax; move: (alc _ ax); fprops.
Qed.
Lemma card_le_to_ell a b:
cardinalp a -> cardinalp b ->
[\/ a = b, a <c b | b <c a].
Proof.
move=> ca cb.
rewrite /cardinal_lt /cardinal_le.
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 card_le_to_el a b:
cardinalp a -> cardinalp b ->
a <=c b \/ b <c a.
Proof.
move=> ca cb; case: (card_le_to_ell ca cb).
move=> ->; left; fprops.
by move => [p1 _]; left.
by right.
Qed.
Lemma card_le_to_ee a b:
cardinalp a -> cardinalp b ->
a <=c b \/ b <=c a.
Proof.
move=> ca cb; case: (card_le_to_el ca cb); first by left.
by move =>[p1 _]; right.
Qed.
Lemma cardinal_ordinal_lt1 a x: cardinalp x -> inc a x ->
cardinal a <c x.
Proof.
move => cx ax.
have ox: ordinalp x by apply: OS_cardinal.
move: (ordinal_hi ox ax) => oa.
have [_ h]: cardinalp (cardinal a) by fprops.
have aux: cardinal a \Eq a by fprops.
move: (h _ oa aux) => s1.
move: (ordinal_transitive ox ax) => sax.
split; first by split => //; fprops; apply: (sub_trans s1 sax).
move=> bad; rewrite bad in s1.
exact (ordinal_irreflexive oa (s1 _ ax)).
Qed.
Lemma ordinal_cardinal_le1 x y: x <=o y -> (cardinal x) <=c (cardinal y).
Proof.
move => [pa pb pc]; apply /eq_subset_cardP1; exists x; fprops.
Qed.
Lemma ordinal_cardinal_lt x y: x <c y -> x <o y.
Proof. by move=> [pa pb];split => //; apply: ordinal_cardinal_le. Qed.
Lemma ordinal_cardinal_le2P x y: cardinalp x -> ordinalp y ->
((y <o x) <-> (cardinal y <c x)).
Proof.
move=> cx oy; rewrite -{2} (card_card cx).
move: cx => [ox xp].
split; move => [p1 p2].
move: (ordinal_cardinal_le1 p1) => p5; split => //; dneg p3.
apply: ord_leA => //; split => //; apply: xp => //.
by eqsym; move: p3; move/card_eqP.
case: (ord_le_to_el ox oy) => // p3.
move: (ordinal_cardinal_le1 p3)=> r1; case: p2; co_tac.
Qed.
Lemma ordinals_card_ltP y: cardinalp y ->
forall x, inc x y <-> (ordinalp x /\ (cardinal x) <c y).
Proof.
move => cy x; move: (proj1 cy) => oy.
split.
move /(ord_ltP oy) => xy; move: (proj31_1 xy) => ox;split => //.
by apply /(ordinal_cardinal_le2P cy ox).
move => [ox].
by move /(ordinal_cardinal_le2P cy ox) /(ord_ltP oy).
Qed.
Lemma ordinal_cardinal_le3 x y:
cardinalp x -> cardinalp y -> x <=o y -> x <=c y.
Proof.
move => cx cy h; move: (ordinal_cardinal_le1 h).
by rewrite (card_card cx) (card_card cy).
Qed.
Lemma ordinal_cardinal_lt3 x y:
cardinalp x -> cardinalp y -> x <o y -> x <c y.
Proof. by move=> cx cy [le ne]; split => //; apply: ordinal_cardinal_le3. Qed.
Lemma finite_cP x: finite_c x <-> (cardinalp x /\ x <> succ x).
Proof.
split => [ fx | [cx xsx]].
have cx: cardinalp x by fprops.
split => //.
move: fx => [p1 p2]; dneg h; apply /card_eqP.
rewrite -/(succ x) -h card_card//.
split; first by apply: OS_cardinal.
dneg infx; red in infx; rewrite /succ -{1} (card_card cx).
by apply /card_eqP.
Qed.
Lemma infinite_cP x: infinite_c x <-> (cardinalp x /\ x = succ x).
Proof.
rewrite /infinite_c /succ/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 (succ 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_le_infinite a b: finite_c a -> infinite_c b -> a <=c b.
Proof.
move=> fa [cb].
have ca: (cardinalp a) by fprops.
move: (OS_cardinal cb) => ob.
move/(omega_P1 ob) => ifb.
split => //.
move: fa; move /omega_P2 /ifb => ao.
apply: (ordinal_transitive ob ao).
Qed.
Lemma finite_lt_infinite a b: finite_c a -> infinite_c b -> a <c b.
Proof.
move=> fa ib; split; first by apply: finite_le_infinite.
move=> ab; move: fa ib ; rewrite ab; move => [_ h1][_ h2]; contradiction.
Qed.
Lemma ge_infinite_infinite a b: infinite_c a -> a <=c b -> infinite_c b.
Proof.
move=> [_ p1] [ca cb ab]; split => //.
case: (equal_or_not a b) => eab; first by ue.
move: ca cb => [oa _] [ob _]; apply: infinite_o_increasing p1 => //.
have: a <o b by split => //; rewrite ordinal_le_pr0.
by move /ord_ltP0 => [_ _ ].
Qed.
Theorem le_finite_finite a b: finite_c b -> a <=c b -> finite_c a.
Proof.
move=> fb ab.
have ca: (cardinalp a) by move: ab => [ca _].
case: (finite_dichot ca) => // ia.
move: (finite_lt_infinite fb ia) => ba; co_tac.
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 -> succ x = succ_o x.
Proof.
move=> cx; rewrite /succ.
by rewrite (card_card (CS_succ_o 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.
case: (@infinite_dichot2 omega0); first exact: (sub_finite_set infc fsx).
red; rewrite (card_card CS_omega); exact omega_infinite.
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 <o omega0.
Proof.
move=> ifs; apply /ord_ltP0; 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 ord_ge1P x: (\1o <=o x) <-> (\0o <o x).
Proof.
split; move=> le1; have ox: ordinalp x by ord_tac.
split; first by apply: ozero_least.
move=> xs; rewrite - xs in le1;exact: (card1_nz (ord_le0 le1)).
by rewrite - succ_o_zero; apply /ord_succ_ltP.
Qed.
Lemma ord_ge1 x: ordinalp x -> x <> \0o -> \1o <=o x.
Proof. by move=> ox xne; apply/ord_ge1P; apply: ord_ne0_pos. Qed.
Hint Resolve ord_ge1 : fprops.
Lemma ord_lt1 x: x <o \1o -> x = \0o.
Proof. by move /ord_ltP0=> [_ _ /set1_P]. Qed.
Ltac ord_tac1 :=
match goal with
| h1: ordinalp ?x |- \0o <=o ?x => apply: (ozero_least h1)
| h1: ordinalp ?x, h2: ?x <> \0o |- \0o <o ?x
=> apply: (ord_ne0_pos h1 h2)
| h: ?x <=o \0o |- ?x = \0o => apply: (ord_le0 h)
| h: _ <o ?x |- ?x <> \0o => apply: (ord_gt_ne0 h)
| h: ?x <o \1o |- ?x = \0o => apply: (ord_lt1 h)
| h: \1o <=o ?x |- \0o <o ?x => by apply/ord_ge1P
| h: \0o <o ?x |- \1o <=o ?x => by apply/ord_ge1P
end.
Lemma ord_zero_dichot x: ordinalp x -> x = \0o \/ \0o <o x.
Proof.
move => ox; case: (equal_or_not x \0o) => xe; [by left | right; ord_tac1].
Qed.
Lemma ord_one_dichot x y: x <o y -> (y = \1o \/ \1o <o y).
Proof.
move => h; case: (equal_or_not y \1o) => h'; [by left | right; split; fprops].
apply: ord_ge1; [ord_tac | move=> h''; case: (@ord_lt0 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 card_le0 a: a <=c \0c -> a = \0c.
Proof.
move=> alez; move:(czero_least (proj31 alez))=> zlea; co_tac.
Qed.
Lemma card_lt0 x: x <c \0c -> False.
Proof. by move=> [pa pab]; move: (card_le0 pa). Qed.
Lemma card_ne0_pos x: cardinalp x -> x <> \0c -> \0c <c x.
Proof. move => cx xnz; split => //; [ by apply: czero_least | fprops]. Qed.
Lemma succ_nz n: succ n <> \0c.
Proof. apply: cardinal_nonemptyset1; exists n; fprops. Qed.
Lemma succ_positive a: \0c <c (succ a).
Proof.
split; first by apply: czero_least; apply: CS_succ.
exact: (nesym(@succ_nz a)).
Qed.
Hint Resolve czero_least: fprops.
Lemma succ_zero: succ \0c = \1c.
Proof. rewrite /succ succ_o_zero; apply: card_card; apply: CS1. Qed.
Lemma succ_one: succ \1c = \2c.
Proof. rewrite /succ succ_o_one; apply: card_card; apply: CS2. Qed.
Lemma card_lt_01: \0c <c \1c.
Proof. rewrite - succ_zero; apply: succ_positive. Qed.
Lemma card_le_01: \0c <=c \1c.
Proof. by move: card_lt_01 => [res _]. Qed.
Lemma card_le_12: \1c <=c \2c.
Proof. by split; fprops => // t /set1_P ->; apply:set2_1. Qed.
Lemma card_lt_12: \1c <c \2c.
Proof. split; [ exact:card_le_12 | fprops ]. Qed.
Lemma card_lt_02: \0c <c \2c.
Proof. exact: (card_lt_ltT card_lt_01 card_lt_12). Qed.
Lemma card_ge1P x: (\1c <=c x) <-> (\0c <c x).
Proof.
move: CS0 CS1 => c0 c1.
split; move=> le1; have ox: cardinalp x by co_tac.
apply: ordinal_cardinal_lt3 => //; apply /ord_ge1P.
by apply: ordinal_cardinal_le.
apply: ordinal_cardinal_le3 => //; apply /ord_ge1P.
by apply: ordinal_cardinal_lt.
Qed.
Lemma card_lt1 x: x <c \1o -> x = \0c.
Proof. move=> h; move: (ordinal_cardinal_lt h); apply: ord_lt1. Qed.
Lemma card_ge1 x: cardinalp x -> x <> \0c -> \1c <=c x.
Proof. by move => sa sb; apply /card_ge1P; apply:card_ne0_pos. Qed.
Lemma card_lt2 a: a <c \2c -> a = \0c \/ a = \1c.
Proof.
rewrite /card_two /card_one /card_zero.
move => [[ca _ s2] an2].
case: (emptyset_dichot a) => ae; first by left.
move: ae => [t ta].
case (inc_or_not (singleton emptyset) a) => h1.
have et: inc emptyset (singleton emptyset) by fprops.
move: (ordinal_transitive (proj1 ca) h1 et) => ea; case an2.
by apply: extensionality => // u /set2_P; case => -> //; rewrite - tsi.
case: (equal_or_not t emptyset) => te; last first.
move: (s2 _ ta) => /set2_P; case => // tb; case h1; ue.
right; apply: set1_pr; [ ue | move => u ua].
move: (s2 _ ua) => /set2_P; case => // h2; case h1; ue.
Qed.
Lemma card_ge2 x: cardinalp x -> x <> \0c -> x <> \1c -> \2c <=c x.
Proof.
move => cx x0 x1; case: (card_le_to_el CS2 cx) => //.
by case /card_lt2.
Qed.
Lemma card_le1P E: \1c <=c (cardinal E) <-> nonempty E.
Proof.
split.
rewrite - (card_card CS1).
move /eq_subset_cardP1 /eq_subset_ex_injP=> [f [[ff _] sf tf]].
exists (Vf f emptyset).
rewrite -tf; Wtac; rewrite sf /card_one; fprops.
move=> nE; apply: card_ge1;fprops.
by move=> cEz; case: (cardinal_nonemptyset1 nE).
Qed.
Lemma card_le2P E:
\2c <=c (cardinal E)
<-> exists a b, [/\ inc a E, inc b E & a <> b].
Proof.
split.
rewrite - (card_card CS2).
move /eq_subset_cardP1 /eq_subset_ex_injP => [f [[ff injf] sf tf]].
exists (Vf f emptyset); exists (Vf f (singleton emptyset)).
have ia: inc emptyset (source f) by rewrite sf /card_two; fprops.
have ib: inc (singleton emptyset) (source f) by rewrite sf /card_two; fprops.
rewrite -tf; split; fprops=> h;move: (injf _ _ ia ib h); fprops.
move => [x [y [xE yE nxy]]].
have sE: (sub (doubleton x y) E).
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 x:= Zo (succ_o x) cardinalp.
Definition cardinals_lt x := Zo x (fun z => z <c x).
Lemma cardinals_leP a : cardinalp a ->
forall b, (inc b (cardinals_le a) <-> (b <=c a)).
Proof.
move=> ca b; rewrite/cardinals_le; split.
move /Zo_P => [bs cb]; split => //.
by apply: ordinal_sub3 =>//;apply: OS_cardinal.
move=> [cb _ cs]; apply: Zo_i => //.
by apply/ordinal_sub4P => //; apply: OS_cardinal.
Qed.
Lemma cardinals_ltP x: cardinalp x ->
(forall y, inc y (cardinals_lt x) <-> (y <c x)).
Proof.
move=> cx y; split; first by move /Zo_P => [bs cb].
move => h; move: (ordinal_cardinal_lt h) => yx; apply /Zo_i => //.
by move /(ord_ltP0): yx => [_ _].
Qed.
Lemma CS_sup E: cardinal_set E -> cardinalp (\csup E).
Proof.
move=> alc.
have os: ordinal_set E by move=> t tx; move: (alc _ tx) => [ct _].
move: (OS_sup os) => oe.
apply /cardinalP; split => //; move=> z zE ezE.
move: (ordinal_hi oe zE) => oz.
have p3: forall a, inc a E -> sub a (union E).
by move=> a ax; move: (ord_sup_ub os ax) => [_ _].
have p4: forall c, ordinalp c -> (forall i , inc i E -> i <=o c)
-> sub (union E) c.
by move => c oc h; move: (ord_ub_sup os oc h) => [_ _ ].
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:(ord_le_to_si oa oz) => // za; case: h; ex_tac.
case: (ordinal_irreflexive oz ((p4 _ oz p2) _ zE)).
move: (sub_smaller (p3 _ ax))(os _ ax) => p4a oa.
move: (sub_smaller (ordinal_transitive oa za)) => p5.
move: ezE => /card_eqP => ezE; rewrite ezE in p4a.
have: (cardinal a = cardinal z) by co_tac.
move/card_eqP => cza.
move: (alc _ ax) => [_ p6]; move: (p6 _ (ordinal_hi oa za) cza) => p7.
case: (ordinal_decent oa za (p7 _ za)).
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_ub_sup E : cardinal_set E ->
forall y, cardinalp y -> (forall i, inc i E -> i <=c y) ->
(\csup E) <=c y.
Proof.
move => alc y cy ali; move: (CS_sup alc) => cs; split => //.
have os: ordinal_set E by move=> t tx; move: (alc _ tx) => [ct _].
suff: (\csup E) <=o y by move=> [_ _].
apply: ord_ub_sup => //; first by apply: OS_cardinal.
move=> o ie; move: (ali _ ie); apply: ordinal_cardinal_le.
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 pa: cardinal_set (fun_image E f).
move => t /funI_P [z zE ->]; move: (h _ zE) => aux; co_tac.
have pb: cardinal_set (fun_image E g).
move => t /funI_P [z zE ->]; move: (h _ zE) => aux; co_tac.
apply: card_ub_sup => //; first by apply: CS_sup.
move=> i /funI_P [z zE ->]; apply: (card_leT (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) (card_ub_sup alc) => pa pb pc.
apply /unique_existence; split.
by exists (union x); split => // y cy.
move=> u v [cu up1 up2][cv vp1 vp2].
move: (vp2 _ cu up1)(up2 _ cv vp1) => r1 r2; co_tac.
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].
move: (vp2 _ cu up1)(up2 _ cv vp1) => r1 r2.
co_tac.
Qed.
Lemma surjective_cardinal_le 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].
move:(right_inverse_fi ri) => ii.
move: (right_i_source ri)=> si.
move: ri=> [[_ _ ti] _].
rewrite -tz - sz - si ti.
by apply /eq_subset_ex_injP; exists f.
Qed.
Lemma image_smaller_cardinal f: function f ->
cardinal (image_of_fun f) <=c cardinal (source f).
Proof.
move=> ff.
move: (restriction_to_image_fs ff) => sr.
apply: surjective_cardinal_le.
exists (restriction_to_image f).
by split=>//; rewrite/ restriction_to_image /restriction2; 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_cardinal (proj1 sjb)); rewrite (surjective_pr0 sjb); aw.
Qed.
Lemma image_smaller_cardinal1 f x: function f ->
cardinal (image_by_fun f x) <=c cardinal x.
Proof.
move => pa.
move: (@subsetI2l x (source f)) (@subsetI2r x (source f)) => a1 a2.
have ->: image_by_fun f x = image_by_fun 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_cardinal (proj1 sjb)).
rewrite (surjective_pr0 sjb) /restriction1; aw => le2; co_tac.
Qed.
End Cardinal.
Export Cardinal.