proposition: Theorem c3f_fs u v: (nonempty (source u) \/ (nonempty (source v)) \/ (nonempty (target v)) \/ target u = emptyset) -> injection u -> surjection v -> surjection (compose3function u v).
proof: Proof. move=> nehyp iu sv. have fu: function u by fct_tac. have fv: function v by fct_tac. have c3ff:= (c3f_f fu fv). split => //; rewrite /compose3function; aw => y ys. case: (emptyset_dichot (source u)) => nesu. have p:(target u = emptyset \/ nonempty (source v)). case: nehyp. by rewrite nesu=> [] [h] [x]; case: x. case; [by right | case; last by left]. by move=> [w wt]; move: (surjective_pr sv wt)=> [x xs _];right; ex_tac. have: (nonempty (functions (target u) (source v))). by apply: (fun_set_ne p). move=> [f fsp]; ex_tac; move/functionsP:(fsp) => [ff sf tf]. rewrite c3f_V //. apply: (fun_set_small_source (y:=target v)); rewrite - nesu //. by apply: c3f_axiom. have [s [cvs cvsi]] := (exists_right_inv_from_surj sv). have [r [cru crui]] := (exists_left_inv_from_inj iu nesu). have Hb: function s by fct_tac. have Hc: function r by fct_tac. move/functionsP:ys=> [fy sy ty]. have sf: source ((s \co y) \co r) = target u by move: cru=> [_ _]; aw. have tf: target ((s \co y) \co r) = source v by move: cvs=> [_ _]; aw. have sytr: source y = target r by rewrite sy; move: (f_equal target crui); aw. have tytr: source s = target y by rewrite ty; move: (f_equal source cvsi); aw. have csy: s \coP y by []. have fcyr: function (y \co r) by fct_tac. have csyr: s \coP (y \co r) by hnf; aw. have tcyr : (target (y \co r) = target v) by aw. have fcsy: function (s \co y) by fct_tac. have ff: function ((s \co y) \co r) by fct_tac=>//; aw. exists ((s \co y) \co r) ; first by apply/functionsP. rewrite c3f_V // -(@compfA s y r) // (@compfA v s (y \co r)) //. rewrite cvsi -tcyr compf_id_l // -compfA // crui - sy compf_id_r //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)