proposition: Lemma bij_double_F2 F G a b f g : inc a F -> inc b F -> a <> b -> disjoint F G -> bijection_prop f F (coarse F) -> bijection_prop g F G -> let h := bij_double_F2_fun F G a b f g in bijection_prop h (F \cup G) (coarse (F\cup G)) /\ extends h f.
proof: Proof. move => aF bF anb di fp gp. move:(inverse_bij_bp fp)(inverse_bij_bp gp). set gi := inverse_fun g; set fi := inverse_fun f. move =>[[[ffi ifi] sjfi] sfi tfi] [[[fgi igi] sjgi] sgi tgi]. move:(proj31 gp) => bg;move: gp =>[[[fg ig] [_ sjg]] sg tg]. move: fp =>[[[ff iff] [_ sjf]] sf tf]. set FG := F \cup G. pose H := (G\times F \cup G\times G) \cup F \times G. have Hv: H = G \times FG \cup F\times G. by rewrite /H - set2_UXr. have di1: disjoint (G \times FG) (F \times G). apply:disjoint_pr => u /setX_P[_ pg _] /setX_P[_ pf _];empty_tac1 (P u). have du2: disjoint (coarse F) H. clear di1. rewrite Hv;apply:disjoint_pr => x /setX_P[_ x1 X2]; case/setU2_P. move=> /setX_P[_ y1 y2]; empty_tac1 (P x). move=> /setX_P[_ y1 y2]; empty_tac1 (Q x). set alpha := fun x y => J a (Vf fi (J x (Vf gi y))). have alpha_p0 x y: inc x F -> inc y G -> inc (J x (Vf gi y)) (source fi). move => xE yF; rewrite sfi; apply: setXp_i => //; Wtac. have alpha_p1 x y: inc x F -> inc y G -> inc (alpha x y) (coarse F). move => xE yF; apply: (setXp_i aF); Wtac. have alpha_p2 x y x' y': inc x F -> inc y G -> inc x' F -> inc y' G -> (alpha x y) = (alpha x' y') -> x = x' /\ y = y'. move => qa qb qc qd /pr2_def e1. move:(pr12_def (ifi _ _ (alpha_p0 _ _ qa qb)(alpha_p0 _ _ qc qd) e1)). move=> [qe qf]; split => //; apply: igi; ue. set beta := ( fun y => (Yo (inc y F) (J a y) (J b (Vf gi y)))). have beta_p1 y: inc y FG -> inc (beta y) (coarse F). rewrite /beta; move => yH; Ytac w; apply:setXp_i => //; Wtac. by rewrite sgi;case/setU2_P:yH. have beta_p2 y y': inc y FG -> inc y' FG -> beta y = beta y' -> y = y'. rewrite/beta;move=> yH yH'; Ytac w; Ytac wb; move => /pr12_def [qa qb]. - exact. - by case anb. - by case anb. - by move: qb;apply: igi;rewrite sgi;case/setU2_P:yH=> //; case/setU2_P:yH'. set gamma := fun x y => J b (Vf fi (J (Vf gi x) (Vf fi (beta y)))). have gamma_p0 x y: inc x G -> inc y FG -> inc (J (Vf gi x) (Vf fi (beta y))) (source fi). move => xa yb; rewrite sfi; apply: setXp_i; Wtac. by rewrite sfi; apply beta_p1. have gamma_p1 x y: inc x G -> inc y FG -> inc (gamma x y) (coarse F). move => xa yb; apply: (setXp_i bF); Wtac. have gamma_p2 x y x' y': inc x G -> inc y FG -> inc x' G -> inc y' FG -> gamma x y = gamma x' y' -> x = x' /\ y = y'. move => qa qb qc qd /pr2_def e1. move:(pr12_def (ifi _ _ (gamma_p0 _ _ qa qb) (gamma_p0 _ _ qc qd) e1)). move=> [qz qf]; split; [ apply: igi; ue | apply: beta_p2 => //]. apply: ifi => //;ue. set f2:= fun p => Vf g (Vf fi (Yo (inc (P p) F) (alpha (P p) (Q p)) (gamma (P p) (Q p)))). set f3 := (cantor_bernstein_bij G H (Lf (J a) G H) (Lf f2 H G)). have Hw x: inc x G -> ~ inc x F. by move => qa qb; case: (@in_set0 x); rewrite - di; apply/setI2_P. have delta_p0 p: inc p H -> inc (Yo (inc (P p) F) (alpha (P p) (Q p)) (gamma (P p) (Q p))) (source fi). rewrite Hv sfi ;case/setU2_P => /setX_P[pp pa pb]. by rewrite (Y_false (Hw _ pa)); apply: gamma_p1. by Ytac0;apply: alpha_p1. have delta_p1 p: inc p H -> inc (f2 p) G. move => pg; rewrite /f2;Wtac; rewrite sg; Wtac. by rewrite tfi; apply: delta_p0. have delta_p2 p q: inc p H -> inc q H -> f2 p = f2 q -> p = q. move => pH qH ea. move:(delta_p0 p pH) (delta_p0 q qH) => sa sb. move:(Vf_target ffi sa) (Vf_target ffi sb); rewrite tfi - {2 4} sg => sc sd. move:(ifi _ _ sa sb (ig _ _ sc sd ea)). rewrite Hv in pH qH. case/setU2_P:pH => /setX_P[pp pa pb];case/setU2_P:qH => /setX_P[pq pc pd]. + rewrite (Y_false (Hw _ pa)) (Y_false (Hw _ pc)) => eb. by move: (gamma_p2 _ _ _ _ pa pb pc pd eb) =>[ua ub]; apply:pair_exten. + by rewrite (Y_false (Hw _ pa)); Ytac0;move/pr1_def => ab; case: anb. + by rewrite (Y_false (Hw _ pc)); Ytac0;move/pr1_def => ab; case: anb. + Ytac0; Ytac0 => eb; move: (alpha_p2 _ _ _ _ pa pb pc pd eb) =>[ua ub]. by apply:pair_exten. have cb1: injection_prop (Lf f2 H G) H G. by saw;apply: lf_injective. have cb2: injection_prop (Lf (J a) G H) G H. saw; apply: lf_injective. by rewrite Hv; move => x xG; apply: setU2_2; apply: setXp_i. by move => u v _ _ /pr2_def. move: (CantorBernstein_eff cb2 cb1); rewrite -/f3. move => [[[ff3 if3] [_ sjf3]] sf3 tf3]. have ra: sub F FG by apply: subsetU2l. have uFH: coarse F \cup H = coarse FG. by rewrite Hv (setU2_C (G \times FG)) setU2_A /coarse - set2_UXr - set2_UXl. have rc: sub H (coarse FG) by rewrite - uFH; apply: subsetU2r. pose aux := (fun x => Yo (inc x F) (Vf f x) (Vf f3 x)). have rd t: inc t FG -> ~inc t F -> inc t G by case/setU2_P. have Hu t: inc t G -> inc (Vf f3 t) H by move => itg; Wtac. have ax: lf_axiom aux FG (coarse FG). rewrite/aux; move => x xFG /=; Ytac xf; first by apply: (setX_Sll ra); Wtac. by apply:rc; apply: Hu; apply: rd. set K := Lf aux FG (coarse FG). have Kp: bijection_prop K FG (coarse FG). rewrite /K/aux; saw; apply: lf_bijective. - exact. - move => u v uFG vFG; Ytac uf; Ytac vf. + apply: iff; ue. + move:(rd _ vFG vf) => sa sv. by empty_tac1 (Vf f u); [ Wtac | rewrite sv; apply:Hu ]. + move:(rd _ uFG uf) => sa sv. by empty_tac1 (Vf f v); [ Wtac | rewrite - sv; apply:Hu ]. + by apply: if3; rewrite sf3; apply: rd. - move => y yv;case: (inc_or_not y (coarse F)). rewrite -tf; move/sjf; rewrite sf; move =>[x xf ->]. by exists x; [ apply: ra | Ytac0 ]. move => yc; move: yv; rewrite - uFH; case/setU2_P => //; rewrite -tf3=>yH. move:(sjf3 _ yH); rewrite sf3; move =>[x xs ->]. exists x; first by apply:setU2_2. Ytac xx; [by clear di1 du2; empty_tac1 x | done]. move: (Kp) => [bk sk tk]; have fK: function K by fct_tac. have stk: sub (target f) (target K). by rewrite tf tk; apply: setX_Sll; apply: ra. have ssk: sub (source f) (source K) by rewrite sf sk. split; split => //. apply/(sub_functionP ff fK); split => //. move => t; rewrite sf /K/aux => tF; move:(ra _ tF) => tFG. by rewrite LfV//; Ytac0. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)