``` ```

# Theory of Sets EII-3 Correspondences

Copyright INRIA (2009-2010) Apics Team (Jose Grimm).
``` Require Export set1. Set Implicit Arguments. ```

## EII-3-1 Graphs et correspondences

``` Module Correspondence. ```

``` ```
Properties of the empty set
``` Lemma sub_emptyset : forall x,   sub x emptyset = (x = emptyset). Proof. ir. ap iff_eq. ir. empty_tac. nin (H _ H0). elim x0.   ir. ue. Qed. ```
We say `related r x y` if the pair (x,y) is in the graph
``` Definition related r x y := inc (J x y) r. ```
Proposition 1: existence and uniqueness of range and domain
``` Theorem range_domain_exists: forall r,   is_graph r ->   (exists_unique (fun a=> (forall x, inc x a = (exists y, inc (J x y) r))) &     exists_unique (fun b=> (forall y, inc y b = (exists x, inc (J x y) r)))). Proof. ir. ee. red. ee. exists (domain r). ir. aw.   ir. set_extens. rw H1;wrr H0. rw H0; wrr H1.   red. ee. exists (range r). ir. aw.   ir. set_extens. rw H1; wrr H0. rw H0; wrr H1. Qed. Lemma sub_graph_prod: forall r, is_graph r ->   sub r (product (domain r)(range r)). Proof. ir. red. ir. set (H _ H0). aw. ee. am. ex_tac. ex_tac. Qed. Lemma empty_graph1: forall r, is_graph r ->   (domain r = emptyset) = (r = emptyset). Proof. ir. ap iff_eq; ir; empty_tac.   empty_tac1 (P y). aw. ex_tac. app H.   awi H1. nin H1. rwi H0 H1. elim (emptyset_pr H1). am. Qed. Lemma empty_graph2: forall r, is_graph r ->   (range r = emptyset) = (r = emptyset). Proof. ir. app iff_eq; ir; empty_tac.   empty_tac1 (Q y). aw. ex_tac. app H.   awi H1. nin H1. rwi H0 H1. elim (emptyset_pr H1). am. Qed. ```
A product is a special graph
``` Lemma product_is_graph: forall x y,   is_graph (product x y). Proof. red. ir. awi H. eee. Qed. Hint Resolve product_is_graph: fprops. Lemma product_related: forall x y a b,   related (product x y) a b = (inc a x & inc b y). Proof. ir. uf related. aw. ap iff_eq. int. ir. eee. Qed. Lemma product_domain: forall x y,   nonempty y -> domain (product x y) = x. Proof. ir. set (@product_is_graph x y).   set_extens. awii H0. nin H0. awi H0. int.   aw. nin H. exists y0. fprops. Qed. Lemma product_range: forall x y,    nonempty x -> range (product x y) = y. Proof. ir. set (@product_is_graph x y).   set_extens. awii H0. nin H0. awi H0. int.   aw. nin H. exists y0. fprops. Qed. Lemma constant_function_p1: forall x y,   fgraph (product x (singleton y)). Proof. ir. red. ee. fprops. intros a b. aw. ir. ee. inter2tac. ue. Qed. Lemma emptyset_graph: is_graph (emptyset). Proof. red. ir. nin H. elim x. Qed. Hint Resolve emptyset_graph : fprops. Lemma emptyset_range: range emptyset = emptyset. Proof. rww empty_graph2. fprops. Qed. Lemma emptyset_domain: domain emptyset = emptyset. Proof. rww empty_graph1. fprops. Qed. Lemma emptyset_fgraph: fgraph emptyset. Proof. red. ee. fprops. ir. elim (emptyset_pr H). Qed. Hint Rewrite emptyset_range emptyset_domain : sw. ```
Diagonal of a set: this is a functional graph `x -> x`
``` Definition diagonal x := Zo (product x x)(fun y=> P y = Q y). Lemma diagonal_is_identity: forall x, diagonal x = identity_g x. Proof. ir. uf identity_g. uf L. uf diagonal. set_extens. Ztac. awi H0.   aw. ee. wr (pair_recov H0). rw H1. ex_tac. awi H. nin H. ee. wr H0. Ztac.   fprops. aw. Qed. Lemma inc_diagonal_rw: forall x u,   inc u (identity_g x) = (is_pair u & inc (P u) x & P u = Q u). Proof. ir. wr diagonal_is_identity. uf diagonal.   ap iff_eq; ir; [ idtac | ee] ; Ztac. awi H0. int. aw. wr H1. au. Qed. Lemma inc_pair_diagonal: forall x u v,   inc (J u v) (identity_g x) = (inc u x & u = v). Proof. ir. rw inc_diagonal_rw. aw. ap iff_eq; int. Qed. Hint Rewrite inc_pair_diagonal : aw. Lemma identity_graph: forall x, is_graph (identity_g x). Proof. ir. nin (identity_fgraph x). am. Qed. Hint Resolve identity_graph : fprops. Lemma identity_range: forall x, range (identity_g x) = x. Proof. ir. uf identity_g. set_extens. bwi H. nin H. nin H. ue. bw. ex_tac. Qed. ```
For Bourbaki, a correspondence between A and B is a triple (G,A,B), graph, source and target, with constraints. We use a record, convertible to a triple
``` ```
A triple (G,A,B) or a record F is a correspondence only if G is a subset of the product of A and B. This can be restated as: G is a graph, domain and range are subsets of source and target
``` Definition is_triple f := is_pair f & is_pair (Q f). Definition source x := P (Q x). Definition target x := Q (Q x). Definition graph x := P x. Definition corr_propb s t g:= sub g (product s t). Definition corresp s t g := J g (J s t). Definition is_correspondence f :=   is_triple f & corr_propb (source f) (target f) (graph f). Lemma corr_propa: forall x y z,    corr_propb x y z = inc z (powerset (product x y)). Proof. ir. aw. Qed. Lemma corr_propc: forall s t g,   corr_propb s t g = (is_graph g & sub (domain g) s & sub (range g) t). Proof. ir. sy. uf corr_propb. ap iff_eq; ir. ee.   apw sub_trans (product (domain g) (range g)). ap (sub_graph_prod H).   app product_monotone.   assert (is_graph g). red. ir. cp (H _ H0). awi H1; eee.   ee. am. red. ir. awii H1. nin H1. set (H _ H1). awi i. int.   red. ir. awii H1. nin H1. set (H _ H1). awi i. int. Qed. Lemma is_triple_corr: forall s t g, is_triple (corresp s t g). Proof. red. ir. uf corresp. ee. fprops. aw. fprops. Qed. Lemma corresp_recov: forall f, is_triple f ->   corresp (source f) (target f) (graph f) = f. Proof. ir. nin H. uf corresp. uf source; uf target; uf graph.   app pair_extensionality. fprops. aw. aw. Qed. Lemma corresp_source: forall s t g, source (corresp s t g) = s. Proof. ir. uf corresp; uf source; aw. Qed. Lemma corresp_target: forall s t g, target (corresp s t g) = t. Proof. ir. uf corresp; uf target; aw. Qed. Lemma corresp_graph: forall s t g, graph (corresp s t g) = g. Proof. ir. uf corresp; uf graph; aw. Qed. Hint Rewrite corresp_source corresp_target corresp_graph : aw. Lemma corresp_create: forall s t g,   corr_propb s t g -> is_correspondence (corresp s t g). Proof. ir. red. split. app is_triple_corr. aw. Qed. Lemma corresp_propb: forall f,   is_correspondence f -> corr_propb (source f) (target f)(graph f). Proof. ir. red in H. int. Qed. ```
Some properties of a correspondence
``` Lemma corresp_is_graph: forall g,   is_correspondence g -> is_graph (graph g). Proof. ir. red in H. rwi corr_propc H. eee. Qed. Lemma corresp_sub_range: forall g,   is_correspondence g -> sub (range (graph g)) (target g). Proof. ir. red in H. rwi corr_propc H. eee. Qed. Lemma corresp_sub_domain: forall g,   is_correspondence g -> sub (domain (graph g)) (source g). Proof. ir. red in H. rwi corr_propc H. eee. Qed. Hint Resolve corresp_sub_range corresp_sub_domain corresp_is_graph: fprops. ```
The set of correspondences `E->F` is the product of P and singleton E and singleton F, where P is `powerset (product E F)` is the set of graphs of correspondences
``` Definition set_of_correspondences (x y:Set) :=   product (powerset (product x y))           (product (singleton x) (singleton y)). Lemma set_of_correspondences_rw: forall x y z,   inc z (set_of_correspondences x y) =   (is_correspondence z & source z = x & target z = y). Proof. ir. uf set_of_correspondences. uf is_correspondence.   uf source; uf target; uf graph. uf is_triple. rw corr_propa. aw.   app iff_eq; ir; eee. rw H2; rww H3. rwi H0 H2; rwi H1 H2. am. Qed. Lemma set_of_correspondences_propa: forall f,   is_correspondence f ->   inc f (set_of_correspondences (source f) (target f)). Proof. ir. rw set_of_correspondences_rw. au. Qed. ```
We create a correspondence from a map `f:a->b`
``` Definition gacreate (a b:Set) (f:a->b) := IM (fun y:a => J (Ro y) (Ro (f y))). Definition acreate (a b:Set) (f:a->b) := corresp a b (gacreate f). Lemma acreate_corresp: forall (a b:Set) (f:a->b),   is_correspondence (acreate f). Proof. ir. uf acreate. app corresp_create. red. uf gacreate. red. ir.   nin (IM_exists H). wr H0. aw. ee. fprops. app R_inc. app R_inc. Qed. ```
Image by the graph `r` of a set `u`
``` Definition image_by_graph r u:=   Zo (range r) (fun y=>exists x, inc x u & inc (J x y) r). Definition image_by_fun r u :=   image_by_graph (graph r) u. Definition image_of_fun f :=   image_by_graph (graph f) (source f). Lemma image_by_graph_rw: forall u r y,   inc y (image_by_graph r u) = exists x, (inc x u & inc (J x y) r). Proof. ir. uf image_by_graph. ap iff_eq; ir;Ztac. am.   uf range. aw. nin H. exists (J x y). ee. am. aw. Qed. Hint Rewrite image_by_graph_rw : aw. Lemma sub_image_by_graph: forall u r,   sub (image_by_graph r u) (range r). Proof. ir. uf image_by_graph. ap Z_sub. Qed. Lemma image_by_graph_domain: forall r, is_graph r ->   image_by_graph r (domain r) = range r. Proof. ir. app extensionality. app sub_image_by_graph.   red. ir. aw. awii H0. nin H0. ex_tac. ex_tac. Qed. Lemma image_by_emptyset: forall r,   image_by_graph r emptyset = emptyset. Proof. ir. uf image_by_graph. empty_tac. Ztac. nin H1. ee.   ap (emptyset_pr H1). Qed. Lemma image_by_nonemptyset: forall u r,   is_graph r -> nonempty u -> sub u (domain r)   -> nonempty (image_by_graph r u). Proof. ir. nin H0. set (H1 _ H0). awii i. nin i. exists x. aw. ex_tac. Qed. Theorem image_by_increasing: forall u u' r,   is_graph r -> sub u u' -> sub (image_by_graph r u) (image_by_graph r u'). Proof. ir. uf image_by_graph. red. ir. Ztac. nin H3. ee. ex_tac. app H0. Qed. Lemma image_of_large: forall u r, is_graph r ->   sub (domain r) u -> image_by_graph r u = range r. Proof. ir. app extensionality. app sub_image_by_graph.   wrr image_by_graph_domain. app image_by_increasing. Qed. ```
Section of the graph `r` at `x`
``` Definition im_singleton r x := image_by_graph r (singleton x). Lemma im_singleton_pr: forall r x y,   inc y (im_singleton r x) = inc (J x y) r. Proof. ir. uf im_singleton. ap iff_eq; ir. awi H. nin H. awi H. ee. ue.   aw. ex_tac. fprops. Qed. Hint Rewrite im_singleton_pr : aw. Lemma im_singleton_inclusion: forall r r', is_graph r -> is_graph r' ->   (forall x, sub (im_singleton r x) (im_singleton r' x)) = sub r r'. Proof. ir. app iff_eq; ir; red; ir.   set (H _ H2). wr (pair_recov i). wrr im_singleton_pr. app H1. aw.   aw. awi H2. app H1. Qed. ```

## EII-3-2 Inverse of a correspondence

``` ```
Inverse graph of `r`
``` Definition inverse_graph r :=   Zo (product(range r)(domain r))   (fun y=> inc (J (Q y)(P y)) r). Lemma inverse_graph_is_graph: forall r, is_graph (inverse_graph r). Proof. ir. red. ir. ufi inverse_graph H. Ztac. ap (pair_in_product H0). Qed. Hint Resolve inverse_graph_is_graph: fprops. Lemma inverse_graph_rw: forall r y, is_graph r ->   inc y (inverse_graph r) = (is_pair y & inc (J (Q y)(P y)) r). Proof. ir. app iff_eq. ir. ee. app (inverse_graph_is_graph H0).   ufi inverse_graph H0. Ztac. am. ir. ee. uf inverse_graph. Ztac. aw.   ee. am. ex_tac. ex_tac. Qed. Lemma inverse_graph_alt: forall r, is_graph r ->   inverse_graph r = fun_image r (fun z => J (Q z) (P z)). Proof. ir. set_extens. rwi inverse_graph_rw H0.   aw. nin H0. ex_tac. aw. am.   awi H0. nin H0. ee. rww inverse_graph_rw. wr H1. aw. ee; fprops. app H. Qed. Lemma inverse_graph_pair: forall r x y,   inc (J x y) (inverse_graph r) = inc (J y x) r. Proof. ir. uf inverse_graph. ap iff_eq; ir; Ztac. awi H1. am.   uf range. uf domain. aw. ee. fprops. ex_tac. aw. ex_tac. aw. aw. Qed. Lemma inverse_graph_pr2: forall r x y,   related (inverse_graph r) y x = related r x y. Proof. ir. uf related. app inverse_graph_pair. Qed. Hint Rewrite inverse_graph_pair : aw. Hint Rewrite inverse_graph_pr2: bw. Lemma inverse_graph_involutive: forall r, is_graph r ->   inverse_graph (inverse_graph r) = r. Proof. ir. assert (is_graph (inverse_graph r)). fprops.   set_extens. rwii inverse_graph_rw H1. nin H1. awii H2.   rww inverse_graph_rw. set (H _ H1). split. am. aw. Qed. Lemma range_inverse: forall r, is_graph r ->   range (inverse_graph r) = domain r. Proof. ir. set_extens; aw; awii H0; fprops;nin H0. awi H0;ex_tac.   exists x0. aw. Qed. Lemma domain_inverse: forall r, is_graph r ->   domain (inverse_graph r) = range r. Proof. ir. transitivity (range (inverse_graph (inverse_graph r))).   sy. rww range_inverse. fprops. rww inverse_graph_involutive. Qed. Lemma inverse_graph_emptyset: inverse_graph (emptyset) = emptyset. Proof. uf inverse_graph. aw. srw. wr sub_emptyset. app Z_sub. Qed. Hint Rewrite inverse_graph_emptyset: sw. Lemma inverse_product: forall x y,   inverse_graph (product x y) = product y x. Proof. ir. set (product_is_graph (x:=x) (y:=y)).   set_extens. rwii inverse_graph_rw H. nin H. aw. awi H0. int.   awi H. ee. rww inverse_graph_rw. eee. Qed. Lemma inverse_identity_g: forall x,   inverse_graph (identity_g x) = identity_g x. Proof. ir. uf inverse_graph. rw identity_range; rw identity_domain.   set_extens. Ztac. awi H1. awi H0. ee. wr (pair_recov H0). aw. int.   rwi inc_diagonal_rw H. ee. Ztac. aw. eee. wr (pair_recov H). aw. wr H1. int. Qed. Hint Rewrite inverse_identity_g inverse_product: aw. ```
Inverse correspondence
``` Definition inverse_fun m :=   corresp (target m) (source m) (inverse_graph (graph m)). Lemma inverse_correspondence: forall m,   is_correspondence m -> is_correspondence (inverse_fun m). Proof. ir. uf inverse_fun. app corresp_create. red.   red. ir. ufi inverse_graph H0. Ztac. set (product_pr H1). ee. aw.   red in H. rwi corr_propc H. eee. Qed. Lemma inverse_fun_involutive: forall m,   is_correspondence m -> inverse_fun (inverse_fun m) = m. Proof. ir. assert (is_graph (graph m)). fprops.   uf inverse_fun. uf corresp. uf target; uf source; uf graph.   red in H. ee. nin H. aw. rww inverse_graph_involutive. aw. Qed. Lemma inverse_source: forall f, source (inverse_fun f) = target f. Proof. ir. uf inverse_fun. aw. Qed. Lemma inverse_target: forall f, target (inverse_fun f) = source f. Proof. ir. uf inverse_fun. aw. Qed. Hint Rewrite inverse_source inverse_target : aw. Hint Resolve inverse_correspondence: fprops. ```
Inverse image by a graph r of a set x
``` Definition inv_image_by_graph r x :=   image_by_graph (inverse_graph r) x. Definition inv_image_by_fun r x:=   inv_image_by_graph(graph r) x. Lemma inv_image_by_fun_pr: forall r x,   inv_image_by_fun r x = image_by_fun (inverse_fun r) x. Proof. ir. uf inv_image_by_fun. uf inverse_fun. uf image_by_fun.   uf corresp. uf graph. aw. Qed. Lemma inv_image_graph_rw: forall x r y,   (inc y (inv_image_by_graph r x)) = (exists u, inc u x & inc (J y u) r). Proof. ir. uf inv_image_by_graph. aw. uf related. ap iff_eq; ir; nin H.   awi H. nin H. ex_tac. nin H. ex_tac. aw. Qed. Hint Rewrite inv_image_graph_rw: aw. ```

## EII-3-3 Composition of two correspondences

``` ```
Composition of two graphs
``` Definition compose_graph r' r :=   Zo (product(domain r)(range r'))   (fun w => exists y, (inc (J (P w) y) r & inc (J y (Q w)) r')). Lemma composition_is_graph: forall r r',   is_graph (compose_graph r r'). Proof. ir. red. ir. ufi compose_graph H. Ztac. ee. ap (pair_in_product H0). Qed. Hint Resolve composition_is_graph: fprops. Lemma inc_compose: forall r r' x,   inc x (compose_graph r' r) =   (is_pair x &( exists y, inc (J (P x) y) r& inc (J y (Q x)) r')). Proof. ir. uf compose_graph. ap iff_eq; ir. Ztac. split.   ap (pair_in_product H0). am.   ee. nin H0. ee. Ztac. uf domain. uf range. aw. ee. am.   ex_tac. aw. ex_tac. aw. ex_tac. Qed. Hint Rewrite inc_compose: aw. Lemma compose_related: forall r r' x z,   (related (compose_graph r' r) x z=   exists y, related r x y & related r' y z). Proof. ir. uf related. ap iff_eq; ir. awi H; int. aw; eee. Qed. Hint Rewrite compose_related: aw. Lemma compose_domain1: forall r r',   sub (domain (compose_graph r' r)) (domain r). Proof. ir. red. ir. awi H. nin H. ufi compose_graph H. Ztac.   rwi product_inc_rw H0. ee. rwii pr1_pair H2. fprops. Qed. Lemma compose_range1: forall r r',   sub (range (compose_graph r' r)) (range r'). Proof. ir. red. ir. awi H. nin H. ufi compose_graph H.   Ztac. rwi product_inc_rw H0. ee. rwii pr2_pair H3. fprops. Qed. ```
Proposition 3, inverse of composition
``` Theorem inverse_compose:forall r r',   inverse_graph (compose_graph r' r) =   compose_graph (inverse_graph r)(inverse_graph r'). Proof. ir.   set_extens. aw. rwii inverse_graph_rw H. ee. am. awi H0.   ee. nin H1. exists x0. aw. int. fprops.   awi H. ee. nin H0. awi H0. ee. wr (pair_recov H). aw. ee. fprops. ex_tac. Qed. ```
Proposition 4, associativity of composition
``` Theorem composition_associative: forall r r' r'',   compose_graph r'' (compose_graph r' r) =   compose_graph (compose_graph r'' r') r. Proof. ir.   set_extens; awi H; ee; nin H0; ee; [awi H0 | awi H1] ; ee; nin H2; ee; aw.   ee. am. exists x1. ee. am. aw. ee. fprops. ex_tac.   ee. am. ex_tac. aw. ee. fprops. ex_tac. Qed. ```
Proposition 5 Image of composition
``` Theorem image_composition: forall r r' x,   image_by_graph(compose_graph r' r) x = image_by_graph r' (image_by_graph r x). Proof. ir.   set_extens. awi H. nin H. ee. awi H0. nin H0. ee. nin H1. ee.   aw. ex_tac. aw. ex_tac.   awi H. nin H. ee. awi H. ee. nin H. ee. aw. ex_tac. aw. ee. fprops. ex_tac. Qed. ```
More properties of composition
``` Lemma compose_domain:forall r r',   is_graph r' ->   domain (compose_graph r' r) = inv_image_by_graph r (domain r'). Proof. ir. set (@composition_is_graph r' r).   set_extens. awii H0. nin H0. awi H0. nin H0. nin H1. ee.   aw. ex_tac. ex_tac.   awi H0. nin H0. ee. awii H0. nin H0. aw. exists x1. aw.   ee. fprops. ex_tac. Qed. Lemma compose_range: forall r r',   is_graph r ->   range (compose_graph r' r) =   image_by_graph r' (range r). Proof. ir. set (@composition_is_graph r' r).   set_extens. awii H0. nin H0. awi H0. ee. nin H1. ee. aw. ex_tac. ex_tac.   awi H0. nin H0. ee. awii H0. nin H0. ee. aw. exists x1. aw. ee.   fprops. ex_tac. Qed. Lemma inverse_direct_image: forall r x,   is_graph r -> sub x (domain r) ->   sub x (inv_image_by_graph r (image_by_graph r x)). Proof. ir. red. ir. set (H0 _ H1). awii i. nin i.   aw. ex_tac. aw. ex_tac. Qed. Lemma composition_increasing: forall r r' s s',   sub r s -> sub r' s' -> sub (compose_graph r' r) (compose_graph s' s). Proof. ir. red; ir. awi H1. ee. nin H2. ee. aw. ee. am.   set (H0 _ H3). ex_tac. app H. Qed. ```
Composition of two correspondences
``` Definition composableC r' r :=   is_correspondence r & is_correspondence r' & source r' = target r. Definition compose r' r :=   corresp (source r)(target r') (compose_graph (graph r')(graph r)). Lemma compose_correspondence: forall r' r,   is_correspondence r -> is_correspondence r' ->   is_correspondence (compose r' r). Proof. ir. uf compose. app corresp_create. red in H. red in H0. ee.   red. red. ir. awi H3. nin H3; nin H4. nin H4.   set (H2 _ H4). awi i. set (H1 _ H5). awi i0. aw. int. Qed. Lemma compose_of_sets: forall r' r x,   image_by_fun(compose r' r) x = image_by_fun r' (image_by_fun r x). Proof. ir. uf image_by_fun.   assert (graph (compose r' r) = compose_graph (graph r') (graph r)).   uf compose. uf corresp. uf graph. aw. rw H. app image_composition. Qed. Lemma inverse_compose_cor: forall r r',   inverse_fun (compose r' r) = compose (inverse_fun r)(inverse_fun r'). Proof. ir. uf inverse_fun. uf compose. uf corresp. uf source; uf target;   uf graph. aw. rww inverse_compose. Qed. ```
Identity correspondence, will be shown to be a function later
``` Definition identity x := corresp x x (identity_g x). Lemma identity_corresp: forall x,   is_correspondence (identity x). Proof. ir. uf identity. app corresp_create. red.   wr diagonal_is_identity. uf diagonal. app Z_sub. Qed. Lemma identity_source: forall x, source (identity x) = x. Proof. ir. uf identity. aw. Qed. Lemma identity_target: forall x, target (identity x) = x. Proof. ir. uf identity. aw. Qed. Hint Rewrite identity_source identity_target: aw. Lemma compose_identity_left: forall m,    is_correspondence m -> compose (identity (target m)) m = m. Proof. ir. uf compose.   assert (compose_graph (identity_g(target m)) (graph m) = graph m).   set_extens. awi H0. ee. nin H1. ee. awi H2. ee. rwi H3 H1. awii H1.   assert (is_graph (graph m)). fprops. set (H1 _ H0).   aw. ee. am. exists (Q x). eee. rww (pair_recov i).   assert (sub (range (graph m)) (target m)). fprops. aw. eee. app H2.   aw. ex_tac.   assert (graph (identity (target m)) = (identity_g (target m))).   uf identity. uf corresp. uf graph. aw. rw H1. rw H0.   uf identity. aw. ap corresp_recov. nin H; am. Qed. Lemma compose_identity_right: forall m,   is_correspondence m -> compose m (identity (source m)) = m. Proof. ir. assert (is_graph (graph m)). fprops. uf compose. uf identity. aw.   assert (Ha:is_graph (identity_g (source m))). fprops.   assert (compose_graph (graph m) (identity_g (source m))= graph m).   set_extens. awi H1. ee. nin H2. ee. awi H2. ee. wri H4 H3.   awi H3. am. am. set (H0 _ H1). aw. ee. am. exists (P x). aw.   assert (sub (domain (graph m))(source m)). fprops. eee. app H2.   aw. ex_tac. rww H1. app corresp_recov. nin H;am. Qed. Lemma compose_identity_identity: forall x,   compose (identity x) (identity x) = (identity x). Proof. ir. set (@identity_corresp x). set (compose_identity_right i). awii e. Qed. Lemma identity_self_inverse: forall x,   inverse_fun (identity x) = (identity x). Proof. ir. uf inverse_fun. uf identity. aw. Qed. End Correspondence. Export Correspondence. ```

## EII-3-4 Functions

``` Module Bfunction. Import Correspondence. ```
This is a different but equivalent definition
``` Definition functional_graph r :=   forall x y y', related r x y -> related r x y' -> y=y'. Lemma is_functional: forall r,   (is_graph r & functional_graph r) = (fgraph r). Proof. ir. uf functional_graph. uf related. app iff_eq. ir. ee. red. ee. am.   ir. assert (J (P x) (Q x) = x). aw. app H.   assert (J (P y) (Q y) = y). aw. app H.   wri H4 H1. wri H5 H2. wri H3 H2. set (H0 _ _ _ H1 H2).   wr H4; wr H5; rw H3; rw e. tv.   ir. split. fprops. ir. app (fgraph_pr H H0 H1). Qed. ```
A function is a correspondence with a functional graph whose source is the domain of the graph
``` Definition is_function f :=   is_correspondence f &   fgraph (graph f) & source f = domain (graph f). Lemma is_function_pr: forall s t g,   fgraph g -> sub (range g) t -> s = domain g ->   is_function (corresp s t g). Proof. ir. uf is_function. aw. eee. app corresp_create.   rw corr_propc. nin H. eee. Qed. Lemma function_fgraph: forall f ,   is_function f -> fgraph (graph f). Proof. ir. red in H. ee. am. Qed. Lemma function_graph: forall f,   is_function f -> is_graph (graph f). Proof. ir. red in H. ee. red in H. eee. Qed. Lemma f_domain_graph: forall f, is_function f -> domain (graph f) = source f. Proof. ir. sy. red in H. eee. Qed. Lemma f_range_graph: forall f, is_function f -> sub (range (graph f))(target f). Proof. ir. red in H. eee. Qed. Hint Rewrite f_domain_graph : aw. Hint Resolve function_graph function_fgraph : fprops. ```
Bourbaki functions as a record
``` Record functionT : Type :=   function_t {sourceT : Set;     targetT : Set;     graphT: Set;     functionT_fgraph: fgraph graphT;     functionT_src: domain graphT = sourceT;     functionT_trg: sub (range graphT) targetT }. Definition functionT_fun (f:Set) (H: is_function f) :=   function_t (function_fgraph H)(f_domain_graph H)(f_range_graph H). Definition corresp_functionT f :=   corresp (sourceT f) (targetT f) (graphT f). Lemma source_T: forall f, sourceT f = source (corresp_functionT f). Proof. ir. uf corresp_functionT. aw. Qed. Lemma target_T: forall f, targetT f = target (corresp_functionT f). Proof. ir. uf corresp_functionT. aw. Qed. Lemma graph_T: forall f, graphT f = graph (corresp_functionT f). Proof. ir. uf corresp_functionT. aw. Qed. Hint Rewrite source_T graph_T target_T : aw. Lemma corresp_functionT_prop: forall f,   is_function (corresp_functionT f). Proof. ir. red. ee. uf corresp_functionT. app corresp_create. rw corr_propc.   split. assert (fgraph (graphT f)). nin f. simpl. am. fprops.   nin f. simpl. rw functionT_src0. eee. uf corresp_functionT. nin f. simpl.   aw. uf corresp_functionT. rw corresp_graph. rw corresp_source. nin f. sy; am. Qed. Hint Resolve corresp_functionT_prop: fprops. Lemma image_by_fun_source: forall f, is_function f ->   image_by_fun f (source f) = range (graph f). Proof. ir. uf image_by_fun. wrr f_domain_graph.   app image_by_graph_domain. fprops. Qed. Lemma related_inc_source: forall f x y,   is_function f -> related (graph f) x y -> inc x (source f). Proof. ir. red in H0. red in H. ee. ue. set (u:=graph f). aw. ex_tac. fprops. Qed. ```
The value of the function `f` at `x` is `W x f`
``` Definition W x f := V x (graph f). Lemma W_pr3: forall f x,   is_function f -> inc x (source f) -> inc (J x (W x f)) (graph f). Proof. ir. uf W. app fdomain_pr1. fprops. aw. Qed. Lemma in_graph_W: forall f x,   is_function f -> inc x (graph f) -> x = (J (P x) (W (P x) f)). Proof. ir. uf W. app in_graph_V. fprops. Qed. Lemma W_pr2: forall f x, is_function f ->   inc x (graph f) -> Q x = W (P x) f. Proof. ir. uf W. app pr2_V. fprops. Qed. Lemma W_pr: forall f x y, is_function f ->   inc (J x y) (graph f) -> W x f = y. Proof. ir. set (in_graph_W H H0). awi e. inter2tac. Qed. Lemma range_inc_rw: forall f y, is_function f ->   inc y (range (graph f)) = exists x, (inc x (source f) & y = W x f). Proof. ir. uf W. rww frange_inc_rw. aw. fprops. Qed. Lemma inc_W_range_graph: forall f x, is_function f -> inc x (source f)   -> inc (W x f) (range (graph f)). Proof. ir. rww range_inc_rw. ex_tac. Qed. Lemma inc_W_target: forall f x, is_function f -> inc x (source f)   -> inc (W x f) (target f). Proof. ir. cp (inc_W_range_graph H H0). nin H.   nin H. rwi corr_propc H3. ee. app H6. Qed. Hint Resolve inc_W_target : fprops. Lemma inc_pr1graph_source: forall f x y, is_function f ->   inc (J x y) (graph f) -> inc x (source f). Proof. ir. app (related_inc_source H H0). Qed. Lemma inc_pr2graph_target: forall f x y, is_function f ->   inc (J x y) (graph f) -> inc y (target f). Proof. ir. wr (W_pr H H0). cp (inc_pr1graph_source H H0). fprops. Qed. Lemma inc_pr1graph_source1:forall f x, is_function f ->   inc x (graph f) -> inc (P x) (source f). Proof. ir. cp (in_graph_W H H0). rwi H1 H0. ap (inc_pr1graph_source H H0). Qed. Lemma inc_pr2graph_target1:forall f x, is_function f ->   inc x (graph f) -> inc (Q x) (target f). Proof. ir. cp (in_graph_W H H0). rw H1. aw. app inc_W_target.   app inc_pr1graph_source1. Qed. Lemma W_image: forall f x y, is_function f -> sub x (source f) ->   (inc y (image_by_fun f x) = exists u, inc u x & W u f = y). Proof. ir. uf image_by_fun. aw. app iff_eq.   ir. nin H1. ee. red in H2. ex_tac. ee. app W_pr. ir.   nin H1. ee. ex_tac. red. wr H2. app W_pr3. app H0. Qed. Hint Rewrite W_image : aw. Ltac graph_tac :=   match goal with     | |- inc (J ?x (W ?x ?f)) (graph ?f) => app W_pr3 ; fprops     | h:inc (J ?x ?y) (graph ?f) |- W ?x ?f = ?y => app W_pr ; fprops     | h:inc (J ?x ?y) (graph ?f) |- ?y = W ?x ?f => sy; app W_pr ; fprops     | |- inc (W _ ?f) (range (graph ?f)) => app inc_W_range_graph ; fprops     | |- inc (W _ ?f) (target ?f) => app inc_W_target ; fprops     | Ha:is_function ?X1, Hb: inc (J _ ?X2) (graph ?X1)       |- inc ?X2 (target ?X1)         => ap (inc_pr2graph_target Ha Hb)     | Ha:is_function ?X1, Hb: inc (J ?X2 _) (graph ?X1)       |- inc ?X2 (source ?X1)         => ap (inc_pr1graph_source Ha Hb)     | Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)       |- inc (P ?X2) (source ?X1)         => ap (inc_pr1graph_source1 Ha Hb)     | Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)       |- inc (Q ?X2) (target ?X1)         => ap (inc_pr2graph_target1 Ha Hb)   end. Definition WT x f:= W x (corresp_functionT f). Lemma defined_lemT: forall f x,   inc x (sourceT f) -> inc (J x (WT x f)) (graphT f). Proof. ir. awi H. uf WT. aw. graph_tac. Qed. Lemma inc_W_targetT: forall f x, inc x (sourceT f)   -> inc (WT x f) (targetT f). Proof. ir. awi H. uf WT. aw. fprops. Qed. Lemma is_function_functional: forall f, is_correspondence f->   is_function f = (forall x, inc x (source f) ->     exists_unique (fun y => related (graph f) x y)). Proof. ir. uf related. ap iff_eq; ir. split. exists (W x f). graph_tac.   ir. nin H0. nin H4. nin H4. set (H6 _ _ H2 H3). awi e.   set (e (refl_equal x)). inter2tac.   ir. red. split. am. red in H. rwi corr_propc H.   set (g:=graph f) in *. ee. red. split. am. ir.   assert (inc (P x) (source f)). app H2. aw. exists (Q x). aw. app H1.   nin (H0 _ H7). set (H1 _ H4). set (H1 _ H5). inter2tac.   app H9. aw. rw H6. aw.   app extensionality. red. ir. aw. nin (H0 _ H4). am. Qed. Lemma image_of_fun_pr: forall f, image_of_fun f = image_by_fun f (source f). Proof. ir. tv. Qed. Lemma sub_image_target:   forall f, is_function f -> sub (image_of_fun f) (target f). Proof. ir. rw image_of_fun_pr. red. ir. awii H0. nin H0. nin H0. wr H1.   fprops. fprops. Qed. Lemma sub_image_target1: forall g x, is_function g ->   sub (image_by_fun g x) (target g). Proof. ir. apw sub_trans (range (graph g)). uf image_by_fun.   app sub_image_by_graph. fprops. nin H. fprops. Qed. ```
The image of singleton by a function is a singleton
``` Lemma image_singleton: forall f x,   is_function f -> inc x (source f) ->   image_by_fun f (singleton x) = singleton (W x f). Proof. ir. set (sub_singleton H0).   set_extens. aw. awi H1. nin H1.   nin H1. wr H2. db_tac. am. am.   aw. exists x. split. fprops. db_tac. Qed. ```
A lemma that says when two functions are equal
``` Lemma function_exten3: forall f g,   is_function f -> is_function g -> graph f = graph g ->   target f = target g -> source f = source g ->   f = g. Proof. ir. nin H. nin H. wr (corresp_recov H). nin H0. nin H0.   wr (corresp_recov H0). ue; ue; ue. Qed. Lemma function_exten1: forall f g,   is_function f -> is_function g -> graph f = graph g ->   target f = target g ->   f = g. Proof. ir. app function_exten3. do 2 wrr f_domain_graph. ue. Qed. Lemma function_exten: forall f g,   is_function f -> is_function g -> source f = source g ->   target f = target g -> (forall x, inc x (source f) -> W x f = W x g)   -> f = g. Proof. ir. app function_exten3. set_extens.   assert (inc (P x) (source f)). graph_tac.   rw (in_graph_W H H4). rww H3. graph_tac. ue.   assert (inc (P x) (source g)). graph_tac. wri H1 H5.   rw (in_graph_W H0 H4). wrr H3. graph_tac. Qed. Lemma inv_image_complement: forall g x,   is_function g ->   inv_image_by_fun g (complement (target g) x) =   complement (source g) (inv_image_by_fun g x). Proof. ir. assert (is_graph (graph g)). fprops.   uf inv_image_by_fun. set_extens. awi H1. nin H1. ee.   srwi H1; ee. srw. ee. graph_tac. dneg. awi H4. nin H4. ee.   assert (fgraph (graph g)). fprops. rww (fgraph_pr H6 H2 H5).   srwi H1; ee. aw. assert (inc (J x0 (W x0 g))(graph g)).   graph_tac. ex_tac. srw. split. fprops. dneg. aw. ex_tac. Qed. ```
The correspondence `acreate f` is a function
``` Lemma prop_acreate: forall (A B:Set) (f:A->B) x,   inc x (graph (acreate f)) = exists u:A, J (Ro u) (Ro (f u)) = x. Proof. ir. uf acreate. aw. uf gacreate. app iff_eq. ir. nin (IM_exists H).   exists x0. am. ir. nin H. app IM_inc. exists x0. am. Qed. Lemma acreate_fgraph : forall (A B:Set) (f:A->B), fgraph(graph (acreate f)). Proof. ir. red. ee. set (acreate_corresp f). fprops. ir.   rwi prop_acreate H. rwi prop_acreate H0. nin H; nin H0.   replace x in *. replace y in *. awi H1. rww (R_inj H1). Qed. Lemma domain_IM: forall (A:Set) (f:A->Set),    A = domain (IM (fun y : A => J (Ro y) (f y))). Proof. ir. uf domain. set_extens. aw. exists (J x (f (Bo H))). split.   app IM_inc. exists (Bo H). rww B_eq. aw. awi H. nin H. nin H.   nin (IM_exists H). wri H1 H0. awi H0. wr H0. app R_inc. Qed. Lemma acreate_function : forall (A B:Set) (f:A->B),   is_function (acreate f). Proof. ir. red. ee. app acreate_corresp. ap (acreate_fgraph f).   uf acreate. rw corresp_graph. aw. uf gacreate. wrr domain_IM. Qed. Hint Resolve acreate_function: fprops. Lemma acreate_W : forall (A B:Set) (f:A->B) (x:A),   W (Ro x) (acreate f) = Ro (f x). Proof. ir. assert (inc (Ro x) (source (acreate f))). uf acreate. aw.   app R_inc.   set (W_pr3 (acreate_function f) H). rwi prop_acreate i. nin i.   wr (pr2_def H0). set (pr1_def H0). rww (R_inj e). Qed. ```
We define `bcreate1 f` of type `source f-> target f` so that ` acreate (bcreate1 f) = f`
``` Definition bcreate1 f (H:is_function f) :=   fun x:source f => Bo (inc_W_target H (R_inc x)). Lemma prop_bcreate1: forall f (H:is_function f) (x:source f),   Ro(bcreate1 H x) = W (Ro x) f. Proof. ir. uf bcreate1. app B_eq. Qed. Lemma bcreate_inv1: forall f (H:is_function f),   acreate (bcreate1 H) = f. Proof. ir. app function_exten. fprops. uf acreate; aw. uf acreate; aw.   ir. ufi acreate H0. awi H0. wr (B_eq H0). rw acreate_W. app prop_bcreate1. Qed. Lemma W_mapping: forall f A B (Ha:source f =A)(Hb:target f =B) x,   is_function f -> inc x A -> inc (W x f) B. Proof. ir. wri Ha H0. wr Hb. fprops. Qed. ```
We define `bcreate f a b` of type `a->b`, it satisfies ` acreate (bcreate f a b) = f`
``` Definition bcreate f A B   (H:is_function f)(Ha:source f =A)(Hb:target f =B):=   fun x:A => Bo (W_mapping Ha Hb H (R_inc x)). Lemma prop_bcreate2: forall f A B   (H:is_function f) (Ha:source f=A)(Hb:target f=B)(x:A),   Ro(bcreate H Ha Hb x) = W (Ro x) f. Proof. ir. uf bcreate. app B_eq. Qed. Lemma bcreate_inv2: forall f A B   (H:is_function f) (Ha:source f=A)(Hb:target f=B),   acreate (bcreate H Ha Hb) = f. Proof. ir. app function_exten. fprops. uf acreate. aw. sy;am.   uf acreate; aw; sy; tv.   ir. ufi acreate H0. awi H0. ir. wr (B_eq H0). rw acreate_W. app prop_bcreate2. Qed. Lemma acreate_source: forall (A B:Set) (f:A->B), source (acreate f)= A. Proof. ir. uf acreate. aw. Qed. Lemma acreate_target: forall (A B:Set) (f:A->B), target (acreate f)= B. Proof. ir. uf acreate. aw. Qed. Hint Rewrite acreate_source acreate_target: aw. Lemma bcreate_inv3: forall (A B:Set) (f:A->B),   bcreate (acreate_function f) (acreate_source f)(acreate_target f) = f. Proof. ir. app arrow_extensionality. ir. app R_inj.   rw prop_bcreate2. rww acreate_W. Qed. Lemma bcreate_eq: forall f (H:is_function f),   bcreate1 H = bcreate H (refl_equal (source f)) (refl_equal (target f)). Proof. ir. app arrow_extensionality. ir. app R_inj.   rw prop_bcreate2. rww prop_bcreate1. Qed. ```
Function with empty graph
``` Definition empty_functionC : emptyset -> emptyset := fun x => x. Definition empty_function:= acreate empty_functionC. Lemma empty_function_function: is_function empty_function. Proof. uf empty_function. fprops. Qed. Lemma empty_function_graph: graph empty_function = emptyset. Proof. uf empty_function. uf acreate. aw. uf gacreate. empty_tac.   nin (IM_exists H). elim x. Qed. Lemma special_empty_function: forall f, is_function f ->   graph f = emptyset -> source f = emptyset. Proof. ir. red in H. ee. rw H2. rw H0. srw. Qed. Lemma empty_function_prop:   bcreate empty_function_function (acreate_source empty_functionC)   (acreate_target empty_functionC)   = empty_functionC. Proof. app arrow_extensionality. ir. elim a. Qed. ```
Properties of the identity function
``` Lemma identity_function: forall x,   is_function (identity x). Proof. ir. uf identity. app is_function_pr.   app identity_fgraph. rww identity_range. fprops. rww identity_domain. Qed. Lemma identity_W: forall x y,   inc y x -> W y (identity x) = y. Proof. ir. uf W. uf identity. aw. app identity_ev. Qed. Hint Rewrite identity_W: sw. Hint Resolve identity_function: fprops. Definition identityC (a:Set): a->a := fun x => x. Implicit Arguments identityC []. Lemma identity_prop: forall a, acreate (identityC a) = identity a. Proof. ir. app function_exten. fprops. fprops. Qed. Lemma identity_prop2: forall a,   bcreate (identity_function a) (identity_source a) (identity_target a) =   identityC a. Proof. ir. wr (bcreate_inv3 (identityC a)).   ap arrow_extensionality. ir. app R_inj.   rw prop_bcreate2. rw prop_bcreate2. rww identity_prop. Qed. ```
A set is small if it has zero or one elements
``` Definition small_set x :=   forall u v, inc u x -> inc v x -> u = v. ```
Definition of a constant function and of the constant function
``` Definition is_constant_function f :=   (is_function f) &   (forall x x', inc x (source f) -> inc x' (source f) -> W x f = W x' f). Definition is_constant_functionC x y (f:x->y) := forall a b, f a = f b. Definition constant_functionC x y (a:y) := fun _:x => a. Implicit Arguments constant_functionC []. Definition constant_function (x y a:Set) (H:inc a y) :=   acreate (constant_functionC x y (Bo H)). Implicit Arguments constant_function []. Lemma constant_source: forall x y a (H:inc a y),   source (constant_function x y a H) = x. Proof. ir. uf constant_function. aw. Qed. Lemma constant_target: forall x y a (H:inc a y),   target (constant_function x y a H) = y. Proof. ir. uf constant_function. aw. Qed. Lemma constant_graph: forall x y a (H:inc a y),   graph (constant_function x y a H) = product x (singleton a). Proof. ir. uf constant_function. uf constant_functionC. uf acreate. aw.   set_extens. ufi gacreate H0. nin (IM_exists H0). wr H1. aw. ee. fprops.   app R_inc. rw B_eq. fprops.   uf gacreate. awi H0. ee. app IM_inc. exists (Bo H1).   app pair_extensionality. fprops. aw. ap B_eq. aw. rw H2. ap B_eq. Qed. Lemma constant_function_fun: forall x y a (H: inc a y),   is_function(constant_function x y a H). Proof. ir. uf constant_function. fprops. Qed. Lemma constant_W: forall x y a (H:inc a y) b,   inc b x -> W b (constant_function x y a H) = a. Proof. ir. app W_pr. app constant_function_fun. rw constant_graph. fprops. Qed. Lemma w_constant_functionC: forall x y (a:y) (z:x),   constant_functionC x y a z = a. Proof. tv. Qed. Lemma constant_function_pr: forall f,   is_function f -> (is_constant_function f =     small_set (range (graph f))). Proof. ir. uf small_set. app iff_eq. ir. rwii range_inc_rw H1.   rwii range_inc_rw H2.   nin H1; nin H2. ee. red in H0. ee. rw H4; rw H3. app H5.   ir. red. ir. ee. am. ir. app H0.   ap (inc_W_range_graph H H1). ap (inc_W_range_graph H H2). Qed. Lemma constant_constant_fun: forall x y a (H: inc a y),   is_constant_function(constant_function x y a H). Proof. ir. red. ee. app constant_function_fun.   assert (source (constant_function x y a H) = x). uf constant_function.   aw. tv. rw H0. ir. rww constant_W. rww constant_W. Qed. Lemma constant_fun_constantC: forall x y a,    is_constant_functionC (constant_functionC x y a). Proof. ir. red. ir. tv. Qed. Lemma constant_function_prop2: forall (x y:Set) (a:y),   bcreate (constant_function_fun x (R_inc a)) (constant_source x (R_inc a))   (constant_target x (R_inc a)) = constant_functionC x y a. Proof. ir. wr (bcreate_inv3 (constant_functionC x y a)).   ap arrow_extensionality. ir. app R_inj. rw prop_bcreate2. rw prop_bcreate2.   uf constant_function. rw B_back. tv. Qed. Lemma constant_fun_prC: forall x y (f:x->y)(b:x), is_constant_functionC f ->   exists a:y, f= constant_functionC x y a. Proof. ir. exists (f b). app arrow_extensionality. ir. uf constant_functionC.   app H. Qed. Lemma constant_fun_pr: forall f (H:nonempty(graph f)),   is_constant_function f ->   exists a: target f,   f= constant_function (source f) (target f) (Ro a) (R_inc a). Proof. ir. red in H0. ee.   assert (is_graph (graph f)). fprops.   assert (inc (rep (source f)) (source f)). app nonempty_rep. nin H.   exists (P y). assert (J (P y) (Q y) = y). aw. app H2. wri H3 H. graph_tac.   assert (inc (W (rep (source f)) f) (target f)).   fprops. exists (Bo H4). app function_exten.   app constant_function_fun. uf constant_function. aw.   uf constant_function. rww acreate_target.   ir. rw constant_W. rw B_eq. app H1. am. Qed. ```

## EII-3-5 Restrictions and extensions of functions

``` ```
Composition of Coq function
``` Definition composeC a b c (g:b->c) (f: a->b):= fun x:a => g (f x). Lemma compositionC_associative: forall a b c d (f: c->d)(g:b->c)(h:a->b),   composeC (composeC f g) h = composeC f (composeC g h). Proof. ir. tv. Qed. Lemma compose_id_leftC: forall (a b:Set) (f:a->b),   composeC (identityC b) f = f. Proof. ir. app arrow_extensionality. Qed. Lemma compose_id_rightC: forall (a b:Set) (f:a->b),   composeC f (identityC a) = f. Proof. ir. app arrow_extensionality. Qed. ```
Function associated to set inclusion
``` Definition inclusionC x y (H: sub x y):=   fun u:x => Bo (H (Ro u) (R_inc u)). Lemma inclusionC_pr: forall x y (H: sub x y) (a:x),   Ro(inclusionC H a) = Ro a. Proof. ir. uf inclusionC. ap B_eq. Qed. Lemma inclusionC_identity: forall x,   inclusionC (sub_refl (x:=x)) = identityC x. Proof. ir. app arrow_extensionality. ir. app R_inj. uf identityC.   rw inclusionC_pr. tv. Qed. Lemma inclusionC_compose: forall x y z (Ha:sub x y)(Hb: sub y z),   composeC (inclusionC Hb)(inclusionC Ha) = inclusionC (sub_trans Ha Hb). Proof. ir. app arrow_extensionality. ir. uf composeC.   app R_inj. rw inclusionC_pr. rw inclusionC_pr. rw inclusionC_pr. tv. Qed. ```
Restriction of a Coq function; agreement of subsets
``` Definition restrictionC (x a b:Set) (f:a->b)(H: sub x a) :=   composeC f (inclusionC H). Definition agreeC (x a a' b b':Set) (f:a->b) (f':a'-> b')   (Ha: sub x a)(Hb: sub x a') :=   forall u:x, Ro(restrictionC f Ha u) = Ro(restrictionC f' Hb u). ```
The functions agree on `x` if they take the same value
``` Definition agrees_on x f f' :=   (sub x (source f)) & (sub x (source f')) &   (forall a, inc a x -> W a f = W a f'). Lemma same_graph_agrees: forall f f',   is_function f -> is_function f' -> graph f = graph f' ->   agrees_on (source f) f f'. Proof. ir. assert (source f = source f'). do 2 wrr f_domain_graph. rww H1.   red. wr H2. eee. ir. set (W_pr3 H H3). rwi H1 i. wrr (W_pr H0 i). Qed. Lemma function_exten2: forall f f',   is_function f -> is_function f' ->   (f =f') = ((source f =source f') & (target f= target f') &     (agrees_on (source f) f f')). Proof. ir. app iff_eq. ir. rww H1. eee. red. eee.   ir. ee. app function_exten. red in H3. ee. am. Qed. Lemma sub_function: forall f g,   is_function f -> is_function g ->   (sub (graph f) (graph g)) = (agrees_on (source f) f g). Proof. ir. ap iff_eq. ir. split. fprops. split.   do 2 wrr f_domain_graph. app sub_graph_domain. ir.   wrr (W_pr H0 (H1 _ (W_pr3 H H2))).   ir. ee. red. ir. assert (inc (P x) (source f)). graph_tac.   red in H1. ee. rw (in_graph_W H H2). rww H5. graph_tac. Qed. ```
Restriction of the function to a part of it source
``` Lemma restr_domain2: forall f x,   is_function f-> sub x (source f) ->   domain (restr (graph f) x) = x. Proof. ir. red in H. ee. rww restr_domain1. ue. Qed. Lemma restr_range: forall f x,   is_function f-> sub x (source f) ->   sub (range (restr (graph f) x)) (target f). Proof. ir. uf range. uf restr. red. ir. awi H1. nin H1. nin H1. Ztac.   wr H2. rw (W_pr2 H H3). fprops. Qed. Definition restriction f x :=   corresp x (target f) (restr (graph f) x). Definition restriction1 f x :=   corresp x (image_by_fun f x) (restr (graph f) x). Lemma restriction_function: forall f x,   is_function f -> sub x (source f) ->   is_function (restriction f x). Proof. ir. uf restriction. app is_function_pr. fprops.   app restr_range. rww restr_domain2. Qed. Lemma restriction1_function: forall f x,   is_function f -> sub x (source f) ->   is_function (restriction1 f x). Proof. ir. uf restriction1. app is_function_pr. fprops.   uf range. uf restr. red. ir. awi H1. nin H1. nin H1. Ztac. aw. ex_tac.   wrr (W_pr2 H H3). rww restr_domain2. Qed. Hint Resolve restriction_function restriction1_function: fprops. Lemma restriction_W: forall f x a,   is_function f -> sub x (source f) ->   inc a x -> W a (restriction f x) = W a f. Proof. ir. uf W. uf restriction. aw. bw. fprops. aw. Qed. Lemma restriction1_W: forall f x a,   is_function f -> sub x (source f) ->   inc a x -> W a (restriction1 f x) = W a f. Proof. ir. uf W. uf restriction1. aw. bw. fprops. aw. Qed. ```
`g` extends `f` if its restriction to the source of `f` is `f`
``` Definition extends g f :=   (is_function f) & (is_function g) & (sub (graph f) (graph g))   & (sub (target f)(target g)). Definition extendsC (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a') :=   sub b b' & agreeC g f H (sub_refl (x:=a)). Lemma source_extends: forall f g,   extends g f -> sub (source f) (source g). Proof. ir. red in H. ee. do 2 wrr f_domain_graph. app sub_graph_domain. Qed. Lemma W_extends: forall f g x,   extends g f -> inc x (source f) -> W x f = W x g. Proof. ir. cp (source_extends H).   red in H. ee. assert (inc (J x (W x f)) (graph g)). app H3.   graph_tac. rww (W_pr H2 H5). Qed. Lemma extendsC_pr : forall (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a'),   extendsC g f H -> forall x:a, Ro (f x) = Ro(g (inclusionC H x)). Proof. ir. red in H0. ee. ufi agreeC H1. cp (H1 x).   ufi restrictionC H2. ufi composeC H2. rww H2.   rww inclusionC_identity. Qed. Lemma function_extends_restr: forall f x,   is_function f -> sub x (source f) ->   extends f (restriction f x). Proof. ir. red. ee. fprops. am.   uf restriction. aw. app restr_sub.   uf restriction. aw. fprops. Qed. Lemma function_extends_restC: forall (x a b:Set) (f:a->b)(H:sub x a),   extendsC f (restrictionC f H) H. Proof. ir. red. ee. fprops. red. uf restrictionC.   rw inclusionC_identity. rw compose_id_rightC. tv. Qed. Lemma agrees_same_restriction: forall f g x,   is_function f -> is_function g -> agrees_on x f g ->   target f = target g ->   restriction f x =   restriction g x. Proof. ir. red in H1. ee. apply function_exten. fprops. fprops.   uf restriction. aw. uf restriction. aw.   ir. ufi restriction H5. awi H5.   do 2 rww restriction_W. app H4. Qed. Lemma agrees_same_restrictionC: forall (a a' b x:Set) (f:a->b)(g:a'->b)   (Ha: sub x a)(Hb: sub x a'),   agreeC f g Ha Hb -> restrictionC f Ha = restrictionC g Hb. Proof. ir. red in H. app arrow_extensionality. ir. app R_inj. Qed. Lemma restriction_graph1: forall f x,   is_function f -> sub x (source f) ->   graph (restriction f x) =   intersection2 (graph f)(product x (target f)). Proof. ir. uf restriction. aw. set_extens. awi H1. ee. inter2tac. aw.   assert (is_pair x0). assert (is_graph (graph f)). fprops.   app H3. eee. graph_tac.   aw. nin (intersection2_both H1). split. am. awi H3. int. Qed. Lemma restriction_recovers: forall f x,   is_function f -> sub x (source f) ->   restriction f x = corresp x (target f)     (intersection2 (graph f)(product x (target f))). Proof. ir. wrr (restriction_graph1 H H0). uf restriction. aw. Qed. ```
Restriction of a function on the source and target
``` Definition restriction2 f x y :=   corresp x y (intersection2 (graph f) (product x (target f))). Definition restriction2_axioms f x y :=   is_function f &   sub x (source f) & sub y (target f) & sub (image_by_fun f x) y. Lemma restriction2_graph: forall f x y,   sub (graph (restriction2 f x y)) (graph f). Proof. ir. uf restriction2. aw. app intersection2sub_first. Qed. Lemma inc_graph_restriction2: forall f x y a b,   (inc (J a b) (graph (restriction2 f x y))) =   (inc (J a b) (graph f) & inc a x & inc b (target f)). Proof. ir. uf restriction2. aw. app iff_eq. ir.   nin (intersection2_both H). split. am. awi H1. eee.   ir. ee. inter2tac. fprops. Qed. Lemma restriction2_props: forall f x y,   restriction2_axioms f x y ->   domain (intersection2 (graph f) (product x (target f))) = x. Proof. ir. assert (is_graph (intersection2 (graph f) (product x (target f)))).   red. ir. nin (intersection2_both H0). awi H2. int.   set_extens. awi H1. nin H1. nin (intersection2_both H1). awi H3. int. am.   aw. red in H. ee. exists (W x0 f). inter2tac. graph_tac. aw. eee. Qed. Lemma restriction2_function: forall f x y,   restriction2_axioms f x y ->   is_function (restriction2 f x y). Proof. ir. assert (Ha:=restriction2_props H). red in H. ee. uf restriction2.   set (g := intersection2 (graph f) (product x (target f))).   assert (Hb: fgraph g). uf g. apw sub_graph_fgraph (graph f). fprops.   ap intersection2sub_first.   app is_function_pr. uf g. red. ir. ufi g H3. awi H3. nin H3. app H2.   aw. exists x1. nin (intersection2_both H3). awi H5. eee. graph_tac. fprops.   sy; am. Qed. Hint Resolve restriction2_function: fprops. Lemma restriction2_W: forall f x y a,   restriction2_axioms f x y ->   inc a x -> W a (restriction2 f x y) = W a f. Proof. ir. assert (Ha:=restriction2_props H).   uf W. uf restriction2. aw. nin H. ee. app sub_graph_ev. fprops.   ap intersection2sub_first. ue. Qed. Lemma function_rest_of_prolongation: forall f g,   extends g f -> f = restriction2 g (source f) (target f). Proof. ir. red in H. ee. rwi (sub_function H H0) H1. red in H1. ee.   assert (sub (image_by_fun g (source f)) (target f)).   red. ir. awi H5. nin H5. nin H5. wr H6. wrr H4. fprops. am. am.   assert (restriction2_axioms g (source f) (target f)). red; auto.   app function_exten. fprops.   uf restriction2; aw. uf restriction2; aw.   ir. rww restriction2_W. app H4. Qed. Definition restriction2C (a a' b b':Set) (f:a->b)(Ha:sub a' a)   (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') :=   fun u=> Bo (H u). Lemma restriction2C_pr: forall (a a' b b':Set) (f:a->b)(Ha:sub a' a)   (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') (x:a'),   Ro (restriction2C f Ha H x) = W (Ro x) (acreate f). Proof. ir. uf restriction2C. rw B_eq.   set (y:=inclusionC Ha x). assert (Ro y = Ro x). uf y. uf inclusionC.   rw B_eq. tv. wr H0. rww acreate_W. Qed. Lemma restriction2C_pr1: forall (a a' b b':Set) (f:a->b)   (Ha:sub a' a)(Hb:sub b' b)   (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b'),   composeC f (inclusionC Ha) = composeC (inclusionC Hb) (restriction2C f Ha H). Proof. ir. app arrow_extensionality. ir. uf composeC.   app R_inj. rw inclusionC_pr. rw restriction2C_pr.   cp (inclusionC_pr Ha a0). wr H0. rww acreate_W. Qed. ```

## EII-3-6 Definition of a function by means of a term

``` ```
Function from a to b associated to the mapping f
``` Definition BL f a b :=   corresp a b (L a f). Lemma bl_source : forall f a b, source (BL f a b) = a. Proof. ir. uf BL; uf L; aw. Qed. Lemma bl_target : forall f a b, target (BL f a b) = b. Proof. ir. uf BL; uf L; aw. Qed. Hint Rewrite bl_source bl_target : aw. Lemma bl_graph1: forall f a b c,   inc c (graph (BL f a b)) -> c = J (P c) (f (P c)). Proof. ir. ufi BL H. ufi L H. awi H. nin H. ee. wr H0. aw. Qed. Lemma bl_graph2: forall f a b c,   inc c a -> inc (J c (f c)) (graph (BL f a b)). Proof. ir. uf BL. uf L. aw. ex_tac. Qed. Lemma bl_graph3: forall f a b c,   inc c (graph (BL f a b)) -> inc (P c) a. Proof. uf BL. uf L. ir. awi H. nin H. nin H. wr H0. aw. Qed. Lemma bl_graph4: forall f a b c,   inc c (graph (BL f a b)) -> f (P c) = (Q c). Proof. uf BL. uf L. ir. awi H. nin H. ee. wr H0. aw. Qed. ```
In order for `(BL f a b)` to be a function, the following must be satisfied
``` Definition transf_axioms f a b :=   forall c, inc c a -> inc (f c) b. Lemma bl_function: forall f a b,   transf_axioms f a b -> is_function (BL f a b). Proof. ir. uf BL. app is_function_pr. gprops.   red in H. red. ir. rwi L_range H0. awi H0. nin H0. nin H0. wr H1. app H. bw. Qed. Lemma bl_W: forall f a b c,   transf_axioms f a b -> inc c a-> W c (BL f a b) = f c. Proof. ir. ap W_pr. app bl_function. app bl_graph2. Qed. Hint Rewrite bl_W : aw. Lemma bl_recovers: forall f,   is_function f -> BL (fun z => W z f)(source f)(target f) = f. Proof. ir. assert(transf_axioms (fun z => W z f) (source f) (target f)).   red. ir. fprops. app function_exten;aw. app bl_function. ir. aw. Qed. ```
Functions associated to P and Q
``` Definition first_proj g := BL P g (domain g). Definition second_proj g := BL Q g (range g). Lemma first_proj_W: forall g x,   inc x g -> W x (first_proj g) = P x. Proof. ir. uf first_proj. aw. red. ir. uf domain. aw. ex_tac. Qed. Lemma second_proj_W: forall g x,   inc x g -> W x (second_proj g) = Q x. Proof. ir. uf second_proj. aw. red. ir. uf range. aw. ex_tac. Qed. Lemma first_proj_function:forall g,   is_function (first_proj g). Proof. ir. uf first_proj. app bl_function. red. ir. uf domain. aw. ex_tac. Qed. Lemma second_proj_function :forall g,   is_function (second_proj g). Proof. ir. uf second_proj. app bl_function. red. ir. uf range. aw. ex_tac. Qed. ```

## EII-3-7 Composition of two functions. Inverse function

``` ```
Condition for composition to be a function
``` Definition composable g f :=   is_function g & is_function f & source g = target f. Lemma composable_pr: forall f g, composable g f ->   fcomposable (graph g) (graph f). Proof. ir. red. red in H. ee. fprops. fprops. aw. rw H1. app f_range_graph. Qed. Lemma composable_pr1: forall f g, composable g f ->   graph (compose g f) = fcompose (graph g) (graph f). Proof. ir. cp (composable_pr H). wrr alternate_compose. red in H. ee.   assert (fgraph (graph f)). fprops. assert (fgraph (graph g)). fprops.   uf compose. aw. uf gcompose. uf L. set_extens. awi H5. nin H5. nin H6. ee.   aw. exists (P x). split. graph_tac.   set (pr2_V H3 H6). awi e. wr e. set (pr2_V H4 H7). awi e0. wr e0. aw.   set (ff:= graph f) in *. awi H5. nin H5. ee. awi H5. nin H5.   set (pr2_V H3 H5). awi e. wri e H6.   aw. wr H6. aw. split. fprops. exists x1. split. am. app fdomain_pr1.   aw. rw H2. ufi ff H5. graph_tac. fprops. Qed. Lemma compose_domain:forall g f,   composable g f->   domain (graph(compose g f)) = domain (graph f). Proof. ir. rww composable_pr1. app fcomposable_domain.   app composable_pr. Qed. Lemma compose_source: forall f g, source (compose g f) = source f. Proof. ir. uf compose. aw. Qed. Lemma compose_target: forall f g, target (compose g f) = target g. Proof. ir. uf compose. aw. Qed. Hint Rewrite compose_source compose_target : aw. ```
Proposition 6: composition of functions is a function
``` Theorem compose_function: forall g f, composable g f   -> is_function (compose g f). Proof. ir. cp (composable_pr1 H). cp (compose_domain H). rwi H0 H1.   red in H. ee. ufi compose H0. awi H0.   assert (fgraph (fcompose (graph g) (graph f))). app fcompose_fgraph.   rwi (f_domain_graph H2) H1. symmetry in H1.   uf compose. rw H0.   app is_function_pr. apw sub_trans (range (graph g)).   app fcompose_range. fprops. nin H. fprops. Qed. ```
Definition of injectivity, surjectivity and bijectivity
``` Definition injective f:=   is_function f &   (forall x y, inc x (source f) -> inc y (source f) ->     W x f = W y f -> x = y). Definition surjective f :=   is_function f & image_of_fun f = target f. Definition bijective f :=   injective f & surjective f. ```
We give here here some characterizations of injective, surjective, bijective functions
``` Lemma inj_is_function: forall f, injective f -> is_function f. Proof. ir. nin H; am. Qed. Lemma surj_is_function: forall f, surjective f-> is_function f. Proof. ir. nin H; am. Qed. Lemma bij_is_function: forall f, bijective f-> is_function f. Proof. ir. nin H. nin H. am. Qed. Ltac fct_tac :=   match goal with     | H:bijective ?X1 |- is_function ?X1 => exact (bij_is_function H)     | H:injective ?X1 |- is_function ?X1 => exact (inj_is_function H)     | H:surjective ?X1 |- is_function ?X1 => exact (surj_is_function H)     | H:is_function ?X1 |- is_correspondence ?X1 =>       nin H; am     | H:is_function ?g |- sub (range (graph ?g)) (target ?g)       => nin H; fprops     | H:composable ?X1 _ |- is_function ?X1 => destruct H as [H _ ]; exact H     | H:composable _ ?X1 |- is_function ?X1 => destruct H as [_ [H _ ]]; exact H     | H:composable ?f ?g |- is_function (compose ?f ?g ) =>      ap (compose_function H)     | H:is_function ?f |- is_function (compose ?f ?g ) =>      ap compose_function; red; ee; tv     | H:is_function ?g |- is_function (compose ?f ?g ) =>      ap compose_function; red; ee; tv     | Ha:is_function ?f, Hb:is_function ?g |- ?f = ?g =>       app function_exten   end. ```
More properties of function composition
``` Lemma compose_W: forall g f x, composable g f ->   inc x (source f) -> W x (compose g f) = W (W x f) g. Proof. ir. uf W. rww composable_pr1. app fcompose_ev.   rw fcomposable_domain. aw. red in H; eee. app composable_pr. Qed. Hint Rewrite compose_W: aw. Lemma composable_acreate:forall (a b c:Set) (f: a-> b)(g: b->c),   composable (acreate g) (acreate f). Proof. ir. red. eee. aw. Qed. Lemma compose_acreate:forall (a b c:Set) (g: b->c)(f: a-> b),   compose (acreate g) (acreate f) = acreate(composeC g f). Proof. ir. set (composable_acreate f g).   app function_exten. fct_tac. fprops. aw. aw. aw.   ir. aw. wr (B_eq H). uf composeC. repeat rw acreate_W. tv. Qed. Lemma compose_assoc: forall f g h,   composable f g -> composable g h ->   compose (compose f g) h = compose f (compose g h). Proof. ir.   assert (is_function (compose f g)). fct_tac.   assert (is_function (compose g h)). fct_tac.   assert (composable (compose f g) h). red in H0. red. eee. aw.   assert (composable f (compose g h)). red in H; red; eee. aw.   ap function_exten. fct_tac. fct_tac. aw. aw. aw. aw. ir. aw.   red in H0. ee. rw H7. fprops. Qed. Lemma compose_id_left: forall m,   is_function m-> compose (identity (target m)) m = m. Proof. ir. app compose_identity_left. fct_tac. Qed. Lemma compose_id_right: forall m,   is_function m-> compose m (identity (source m)) = m. Proof. ir. app compose_identity_right. fct_tac. Qed. Lemma injective_pr: forall f x x' y,   injective f -> related (graph f) x y -> related (graph f) x' y -> x = x'. Proof. ir. nin H. app H2. app (related_inc_source H H0).   app (related_inc_source H H1). rw (W_pr H H0). rw (W_pr H H1). tv. Qed. Lemma injective_pr3: forall f x x' y,   injective f -> inc (J x y) (graph f) -> inc (J x' y) (graph f) -> x = x'. Proof. ir. app (injective_pr H H0 H1). Qed. Lemma injective_pr_bis: forall f,   is_function f -> (forall x x' y,   related (graph f) x y -> related (graph f) x' y -> x = x') -> injective f. Proof. ir. red. ee. am. ir. app (H0 x y (W x f)).   ap (W_pr3 H H1). rw H3. ap (W_pr3 H H2). Qed. Lemma surjective_pr: forall f y,   surjective f -> inc y (target f) ->   exists x, inc x (source f) & related (graph f) x y . Proof. ir. red in H. ee. wri H1 H0. ufi image_of_fun H0. awi H0. am. Qed. Lemma surjective_pr2: forall f y,   surjective f -> inc y (target f) -> exists x, inc x (source f) & W x f = y. Proof. ir. nin (surjective_pr H H0). exists x. ee. am. app W_pr. fct_tac. Qed. Lemma surjective_pr3: forall f,   surjective f -> range (graph f) = target f. Proof. ir. app extensionality. nin H. fct_tac.   red. ir. nin (surjective_pr H H0). aw. ee. exists x0. app H2. nin H. fprops. Qed. Lemma surjective_pr4: forall f,   is_function f-> range (graph f) = target f -> surjective f. Proof. ir. red. ee. am. uf image_of_fun. red in H. ee. rw H2.   rww image_by_graph_domain. fprops. Qed. Lemma surjective_pr5: forall f,   is_function f -> (forall y, inc y (target f) ->   exists x, inc x (source f) & related (graph f) x y) -> surjective f. Proof. ir. app surjective_pr4. app extensionality. fct_tac.   red. ir. nin (H0 _ H1). nin H2. red in H3. aw. ex_tac. fprops. Qed. Lemma surjective_pr6: forall f,   is_function f-> (forall y, inc y (target f) ->   exists x, inc x (source f) & W x f = y) -> surjective f. Proof. ir. app surjective_pr5. ir. nin (H0 _ H1). nin H2. ex_tac.   wr H3. red. graph_tac. Qed. Lemma bl_injective: forall f a b, transf_axioms f a b ->   (forall u v, inc u a-> inc v a -> f u = f v -> u = v) ->   injective (BL f a b). Proof. ir. red. ee. app bl_function. aw. ir.   rwii bl_W H3. rwii bl_W H3. app H0. Qed. Lemma bl_surjective: forall f a b, transf_axioms f a b ->   (forall y, inc y b -> exists x, inc x a & f x = y) ->   surjective (BL f a b). Proof. ir. app surjective_pr6. app bl_function. aw. ir.   nin (H0 _ H1). nin H2. ex_tac. rww bl_W. Qed. Lemma bl_bijective: forall f a b, transf_axioms f a b ->   (forall u v, inc u a-> inc v a -> f u = f v -> u = v) ->   (forall y, inc y b -> exists x, inc x a & f x = y) ->   bijective (BL f a b). Proof. ir. split. app bl_injective. app bl_surjective. Qed. Lemma bijective_pr: forall f y,   bijective f -> inc y (target f) ->   exists_unique (fun x=> inc x (source f) & W x f = y). Proof. ir. red in H. red. ee. app surjective_pr2. ir. ee. wri H4 H5.   red in H. ee. app H6. Qed. Lemma function_exten4: forall f g, source f = source g ->   surjective f -> surjective g ->   (forall x, inc x (source f) -> W x f = W x g) -> f = g. Proof. ir. cp (surjective_pr3 H0). cp (surjective_pr3 H1). nin H0; nin H1.   assert (graph f = graph g). app fgraph_exten. fprops. fprops. aw. ir.   awii H7. app (H2 _ H7). fprops. app function_exten1. wr H3; wr H4. rww H7. Qed. ```
Bijectivity of Coq functions
``` Definition injectiveC (a b:Set) (f:a->b) := forall u v, f u = f v -> u =v. Definition surjectiveC (a b:Set) (f:a->b) := forall u, exists v, f v = u. Definition bijectiveC (a b:Set) (f:a->b) := injectiveC f & surjectiveC f. Lemma bijectiveC_pr: forall (a b:Set) (f:a->b) (y:b),   bijectiveC f -> exists_unique (fun x:a=> y = f x). Proof. ir. red in H. ee. uf exists_unique. ee. red in H0. cp (H0 y). nin H1.   exists x. sy. am. red in H. ir. rwi H1 H2. app H. Qed. Lemma bcreate_injective: forall f a b   (H:is_function f)(Ha:source f =a)(Hb:target f =b),   injective f -> injectiveC (bcreate H Ha Hb). Proof. ir. red. ir. red in H0. ee. app R_inj.   app H2. rw Ha. app R_inc. rw Ha. app R_inc.   assert (Ro (bcreate H Ha Hb u) = Ro (bcreate H Ha Hb v)). rw H1. tv.   rwi prop_bcreate2 H3. rwi prop_bcreate2 H3. am. Qed. Lemma bcreate_surjective: forall f a b   (H:is_function f)(Ha:source f =a)(Hb:target f =b),   surjective f -> surjectiveC (bcreate H Ha Hb). Proof. ir. red. ir.   assert (inc (Ro u) (target f)). rw Hb. app R_inc. cp (surjective_pr2 H0 H1).   nin H2. ee. rwi Ha H2. exists (Bo H2). app R_inj. wr H3. rw prop_bcreate2.   rw B_eq. tv. Qed. Lemma bcreate_bijective: forall f a b   (H:is_function f)(Ha:source f =a)(Hb:target f =b),   bijective f -> bijectiveC (bcreate H Ha Hb). Proof. ir. red in H0. ee. red. ee.   app bcreate_injective. app bcreate_surjective. Qed. Lemma bcreate1_injective: forall f (H:is_function f),   injective f -> injectiveC (bcreate1 H). Proof. ir. rw (bcreate_eq H). app bcreate_injective. Qed. Lemma bcreate1_surjective: forall f (H:is_function f),   surjective f -> surjectiveC (bcreate1 H). Proof. ir. rw (bcreate_eq H). app bcreate_surjective. Qed. Lemma bcreate1_bijective: forall f (H:is_function f),   bijective f -> bijectiveC (bcreate1 H). Proof. ir. rw (bcreate_eq H). app bcreate_bijective. Qed. Lemma acreate_injective: forall (a b:Set) (f:a->b),   injectiveC f -> injective (acreate f). Proof. ir. red in H; ee. red. ee. fprops. intros x y Ha Hb.   ufi acreate Ha; awi Ha. ufi acreate Hb; awi Hb.   wr (B_eq Ha). wr (B_eq Hb). rw (acreate_W f (Bo Ha)).   rw (acreate_W f (Bo Hb)). ir. cp (R_inj H0). rww (H _ _ H1). Qed. Lemma acreate_surjective: forall (a b:Set) (f:a->b),   surjectiveC f -> surjective (acreate f). Proof. ir. app surjective_pr6. fprops. aw.    ir. nin (H (Bo H0)).    exists (Ro x). ee. app R_inc. rw acreate_W. rw H1. rw B_eq. tv. Qed. Lemma acreate_bijective: forall (a b:Set) (f:a->b),   bijectiveC f -> bijective (acreate f). Proof. ir. red in H; ee. red. ee. app acreate_injective. app acreate_surjective. Qed. ```
Equipotent means there is a bijection between the sets
``` Definition equipotent x y :=   exists z, bijective z & source z = x & target z = y. Lemma equipotentC: forall x y, equipotent x y = exists f:x->y, bijectiveC f. Proof. ir. app iff_eq. ir. nin H. nin H. assert (is_function x0).   red in H; ee; red in H; ee. am. ee. exists (bcreate H1 H0 H2).   app bcreate_bijective. ir. nin H. red. exists (acreate x0). ee.   app acreate_bijective. aw. aw. Qed. ```
Injectivity and surjectivity of identity and restriction
``` Lemma identity_bijective: forall x,   bijective (identity x). Proof. ir. set (identity_function x).   red. ir. ee. red. ee. am. aw. ir. srwi H1; tv.   app surjective_pr6. aw. ir. exists y. split. am. srw. Qed. Lemma identityC_bijective: forall x,   bijectiveC (identityC x). Proof. red. ir. uf identityC. ee. red. tv. red. ir. exists u. tv. Qed. Lemma restriction2_injective: forall f x y,   injective f -> restriction2_axioms f x y   -> injective (restriction2 f x y). Proof. ir. red. ee. app restriction2_function.   assert (Ht:source (restriction2 f x y) = x). uf restriction2. aw. rw Ht.   ir. rwii restriction2_W H3. rwii restriction2_W H3. nin H. red in H0. ee.   app H4; app H5. Qed. Lemma restriction2_surjective: forall f x y,   restriction2_axioms f x y ->   source f = x -> image_of_fun f = y ->   surjective (restriction2 f x y). Proof. ir. app surjective_pr6. app restriction2_function. ir.   ufi restriction2 H2. awi H2.   ir. wri H1 H2. ufi image_of_fun H2. awi H2. nin H2. ee. exists x0.   rwi H0 H2. ee. uf restriction2. aw. rww restriction2_W. app W_pr.   red in H; eee. Qed. Lemma restriction1_surjective: forall f x,   is_function f -> sub x (source f) ->   surjective (restriction1 f x). Proof. ir. app surjective_pr6. app restriction1_function. ir.   ufi restriction1 H1. awii H1. ufi image_of_fun H1. nin H1. ee.   exists x0. ee. uf restriction1. aw. rww restriction1_W. Qed. Lemma restriction1_bijective: forall f x,   injective f -> sub x (source f) ->   bijective (restriction1 f x). Proof. ir. nin H. split. red. split. app restriction1_function.   assert (Ht:source (restriction1 f x) = x). uf restriction1. aw. rw Ht.   ir. do 2 rwii restriction1_W H4. app H1. app H0. app H0.   app restriction1_surjective. Qed. ```
Extension of a function by adding f(x)=y
``` Definition tack_on_f f x y:=   corresp (tack_on (source f) x)   (tack_on (target f) y) (tack_on (graph f) (J x y)). Lemma tack_on_corresp: forall f x y,   is_correspondence f -> is_correspondence (tack_on_f f x y). Proof. ir. uf tack_on_f. app corresp_create. cp (corresp_propb H). red.   red. ir. rwi tack_on_inc H1. nin H1. set (H0 _ H1). awi i. aw. eee. rw H1.   aw. eee. Qed. Lemma tack_on_function: forall f x y,   is_function f -> ~ (inc x (source f)) -> is_function (tack_on_f f x y). Proof. ir. red in H. ee. uf tack_on_f. app is_function_pr.   app tack_on_fgraph. ue.   rw tack_on_range. red. ir. rwi tack_on_inc H3. nin H3.   assert (sub (range (graph f))(target f)). fprops.   set (H4 _ H3). fprops. rw H3. fprops. rww tack_on_domain. ue. Qed. Hint Resolve tack_on_function: fprops. Lemma tack_on_W_in: forall f x y u,   is_function f -> ~(inc x (source f)) -> inc u (source f) ->   W u (tack_on_f f x y) = W u f. Proof. ir. app W_pr. fprops. uf tack_on_f. aw.   left. graph_tac. Qed. Lemma tack_on_W_out: forall f x y,   is_function f -> ~(inc x (source f)) ->   W x (tack_on_f f x y) = y. Proof. ir. app W_pr. fprops. uf tack_on_f. aw. au. Qed. Lemma tack_on_surjective: forall f x y,   surjective f -> ~(inc x (source f)) -> surjective (tack_on_f f x y). Proof. ir. cp (surj_is_function H). app surjective_pr6. fprops.   ir. ufi tack_on_f H2. awi H2.   assert (source (tack_on_f f x y) = tack_on (source f) x). uf tack_on_f. aw.   rw H3. nin H2. nin (surjective_pr2 H H2). exists x0. eee.   rww tack_on_W_in. exists x. split. fprops. sy. rww tack_on_W_out. Qed. Lemma tack_on_f_injective: forall x f g a b,   is_function f -> is_function g -> target f = target g ->   source f = source g -> ~ (inc x (source f)) ->   (tack_on_f f x a = tack_on_f g x b) -> f = g. Proof. ir. app function_exten. ir. wr (tack_on_W_in a H H3 H5).   rw H4. rwi H2 H3. rwi H2 H5. wr (tack_on_W_in b H0 H3 H5). tv. Qed. ```
Canonical injection of a set into another
``` Definition canonical_injection a b :=   corresp a b (identity_g a). Lemma ci_function: forall a b, sub a b ->   is_function (canonical_injection a b). Proof. ir. uf canonical_injection. app is_function_pr. app identity_fgraph.   rww identity_range. rww identity_domain. Qed. Hint Resolve ci_function : fprops. Lemma ci_W: forall a b x,   sub a b -> inc x a -> W x (canonical_injection a b) = x. Proof. ir. uf W. uf canonical_injection. aw. app identity_ev. Qed. Lemma ci_injective: forall a b,   sub a b -> injective (canonical_injection a b). Proof. ir. red. ee. fprops.   assert (Ht:source (canonical_injection a b) = a).   uf canonical_injection. aw. rw Ht. ir. rwii ci_W H2. rwii ci_W H2. Qed. Lemma ci_range: forall a b, sub a b ->   range (graph (canonical_injection a b)) = a. Proof. ir. uf canonical_injection. aw. rww identity_range. Qed. Lemma inclusionC_injective: forall a b (H: sub a b),   injectiveC (inclusionC H). Proof. red. uf inclusionC. ir. app R_inj.   assert (Ro (Bo (H (Ro u) (R_inc u))) = Ro u). app B_eq.   assert (Ro (Bo (H (Ro v) (R_inc v))) = Ro v). app B_eq.   wr H1; wr H2. rw H0. tv. Qed. ```
Diagonal application
``` Definition diagonal_application a :=   BL (fun x=> J x x) a (product a a). Lemma diag_app_W:forall a x,   inc x a -> W x (diagonal_application a) = J x x. Proof. ir. uf diagonal_application. aw. red. ir. fprops. Qed. Lemma injective_diag_app: forall a,   injective (diagonal_application a). Proof. ir. uf diagonal_application. app bl_injective. red. ir. fprops. ir.   inter2tac. Qed. Lemma diag_app_function: forall a,   is_function (diagonal_application a). Proof. ir. nin (injective_diag_app a). am. Qed. Lemma diag_app_range: forall a,   range (graph (diagonal_application a)) = diagonal a. Proof. ir. rw diagonal_is_identity. uf diagonal_application.   uf BL. aw. set_extens. rwi L_range_rw H. nin H. nin H. wr H0. aw. eee.   rw L_range_rw. rwi inc_diagonal_rw H. ee. ex_tac. app pair_extensionality.   fprops. aw. aw. Qed. ```
Injectivity and surjectivity of P and Q
``` Lemma second_proj_surjective: forall g,   surjective (second_proj g). Proof. ir. app surjective_pr5. app second_proj_function. uf second_proj. aw.   ir. ufi range H. awi H. nin H; nin H. uf BL. uf L. aw.   ex_tac. red. aw. ex_tac. ue. Qed. Lemma first_proj_surjective: forall g ,   surjective (first_proj g). Proof. ir. app surjective_pr5. app first_proj_function. uf first_proj. aw.   ir. ufi domain H. awi H. nin H;nin H. uf BL. uf L. aw.   ex_tac. red. aw. ex_tac. ue. Qed. Lemma first_proj_injective: forall g,   is_graph g -> (injective (first_proj g) = functional_graph g). Proof. ir. assert (is_function (first_proj g)). app first_proj_function.   uf injective. assert (Ht: source (first_proj g) = g). uf first_proj. aw.   rw Ht. app iff_eq. ir. red. ir. red in H2. red in H3. nin H1.   assert (J x y = J x y'). app H4.   rww first_proj_W. rww first_proj_W. aw. inter2tac.   ir. ee. am. ir.   rwii first_proj_W H4. rwii first_proj_W H4. red in H1. ufi related H1.   cp (H _ H2). cp (H _ H3). app pair_extensionality.   rwi is_pair_rw H5. rwi is_pair_rw H6. rwi H5 H2; rwi H6 H3. wri H4 H3.   app (H1 _ _ _ H2 H3). Qed. ```
The function that maps `J x y` to `J y x`
``` Definition inv_graph_canon g :=    BL (fun x=> J (Q x) (P x)) g (inverse_graph g). Lemma inv_graph_canon_W: forall g x,   is_graph g ->inc x g -> W x (inv_graph_canon g) = J (Q x) (P x). Proof. ir. uf inv_graph_canon. aw. red. ir. aw. app H. Qed. Lemma inv_graph_canon_function: forall g,   is_graph g -> is_function (inv_graph_canon g). Proof. ir. uf inv_graph_canon. app bl_function. red. ir. aw. app H. Qed. Lemma inv_graph_canon_bijective: forall g,   is_graph g -> bijective (inv_graph_canon g). Proof. ir. uf inv_graph_canon. app bl_bijective. red; ir.   aw. app H. ir. app pair_extensionality. app H. app H. inter2tac. inter2tac.   ir. rwii inverse_graph_rw H0. ee. ex_tac. aw. Qed. ```
Example 5 page 17 of Bourbaki (page 85 in the English edition)
``` Lemma bourbaki_ex5_17: forall a b,   bijective (BL (fun x=> J x b) a (product a (singleton b))). Proof. ir. app bl_bijective. red. ir.   aw. ee. fprops. am. tv.   ir. inter2tac.   ir. awi H. ee. exists (P y). split. am. wr H1. app pair_recov. Qed. Lemma equipotent_prod_singleton:   forall a b, equipotent a (product a (singleton b)). Proof. ir. exists (BL (fun x=> J x b) a (product a (singleton b))).   ee. app (bourbaki_ex5_17 a b). aw. aw. Qed. Lemma restriction1_pr: forall f,   is_function f -> restriction2 f (source f) (image_by_fun f (source f)) =   restriction1 f (source f). Proof. uf restriction2. uf restriction1. ir.   assert (restr (graph f) (source f) = graph f). ap extensionality.   ap restr_sub. red. ir. rw restr_inc_rw. split. am. graph_tac.   rw H0. nin H. red in H. nin H. red in H2. rwi intersection2_sub H2. rww H2. Qed. ```
Proposition 7 summarizes next two theorems. Let f be a function; then f is a bijection if and only if its inverse is a function
``` Theorem bijective_inv_function: forall f,   bijective f -> is_function (inverse_fun f). Proof. ir. red in H; ee. assert (is_graph (graph f)). nin H; fprops.   uf inverse_fun. app is_function_pr.   red. split. fprops. ir. rwii inverse_graph_rw H2. rwii inverse_graph_rw H3.   ee. wri H4 H5. cp (injective_pr3 H H6 H5). app pair_extensionality.   nin H. rww range_inverse. aw. fprops.   rww domain_inverse. sy; app surjective_pr3. Qed. Theorem inv_function_bijective: forall f,   is_function f -> is_function (inverse_fun f) -> bijective f. Proof. ir. red in H0. ee.   assert (Ha: inverse_graph (graph f) = graph (inverse_fun f)).   uf inverse_fun. aw.   split. app injective_pr_bis. uf related. ir.   wri inverse_graph_pair H3. wri inverse_graph_pair H4. wri Ha H1.   app (fgraph_pr H1 H3 H4).   app surjective_pr4. wr domain_inverse. rw Ha. wr H2.   uf inverse_fun. aw. fprops. Qed. ```
We define here an inverse of `(f:a->b)`
``` Lemma bijective_inv_aux: forall (a b:Set) (f:a->b),   bijectiveC f -> is_function (inverse_fun (acreate f)). Proof. ir. app bijective_inv_function. app acreate_bijective. Qed. Lemma bijective_source_aux: forall (a b:Set) (f:a->b),   source (inverse_fun (acreate f)) = b. Proof. ir. uf inverse_fun. uf acreate. aw. Qed. Lemma bijective_target_aux: forall (a b:Set) (f:a->b),   target (inverse_fun (acreate f)) = a. Proof. ir. uf inverse_fun. uf acreate. aw. Qed. Definition inverseC (a b:Set) (f:a->b)(H:bijectiveC f): b->a :=   bcreate(bijective_inv_aux H)(bijective_source_aux f)   (bijective_target_aux f). Lemma inverseC_pra: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:a),   (inverseC H) (f x) = x. Proof. ir. app R_inj. uf inverseC. rw prop_bcreate2.   wr (acreate_W f). set (g:= acreate f). set (y:= Ro x).   assert (inc y a). uf y. app R_inc.   assert (bijective g). uf g. app acreate_bijective.   assert (is_function g). fct_tac.   app W_pr. app bijective_inv_function. uf inverse_fun. aw.   assert (inc (J (W y g) y) (inverse_graph (graph g))). aw. graph_tac.   uf g. aw. awi H3. am. Qed. Lemma inverseC_prb: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:b),   f ((inverseC H) x) = x. Proof. ir. assert (bijectiveC f). am. nin H0. red in H1.   nin (H1 x). wr H2. rww inverseC_pra. Qed. Lemma inverseC_prc: forall (a b:Set) (f:a-> b) (H:bijectiveC f),   inverse_fun(acreate f) = acreate(inverseC H). Proof. ir. cp (acreate_bijective H).   app function_exten. app bijective_inv_aux. fprops.   uf inverse_fun. uf acreate. aw. uf inverse_fun. uf acreate. aw.   ir. uf inverseC. rww bcreate_inv2. Qed. Lemma bij_left_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,   composeC (inverseC H) f = identityC a. Proof. ir. app arrow_extensionality. ir.   uf composeC. rww inverseC_pra. Qed. Lemma bij_right_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,   composeC f (inverseC H) = identityC b. Proof. ir. app arrow_extensionality. ir.   uf composeC. rww inverseC_prb. Qed. Lemma bijective_double_inverseC: forall (a b:Set) (f:a->b) g g',   composeC g f = identityC a -> composeC f g' = identityC b ->   bijectiveC f. Proof. ir. red. ee. red. ir. transitivity (identityC a u). tv.   wr H. transitivity (identityC a v). wr H. uf composeC. rww H1. tv.   red. ir. exists (g' u). transitivity (identityC b u). wrr H0. tv. Qed. Lemma bijective_double_inverseC1: forall (a b:Set) (f:a->b) g g'   (Ha: composeC g f = identityC a)(Hb: composeC f g' = identityC b),   g = inverseC(bijective_double_inverseC Ha Hb)   & g' = inverseC(bijective_double_inverseC Ha Hb). Proof. ir. assert (g' = g). app arrow_extensionality.   ir. transitivity (identityC a (g' a0)). tv. wr Ha. uf composeC.   assert (f (g' a0) = a0). transitivity (identityC b a0). tv. wrr Hb. tv. rww H.   assert (g = inverseC (bijective_double_inverseC Ha Hb)).   app arrow_extensionality. ir.   assert (f (g' a0) = a0). transitivity (identityC b a0). wrr Hb. tv.   wr H0. rw inverseC_pra. rw H0. sy. rww H. wr H0. intuition. Qed. Lemma bijective_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,   bijectiveC (inverseC H). Proof. ir. red. ee. red. ir. wr (inverseC_prb H u). rw H0.   rw (inverseC_prb H v). tv. red. ir. exists (f u). rww inverseC_pra. Qed. Lemma inverse_fun_involutiveC:forall (a b:Set) (f:a->b) (H: bijectiveC f),   f = inverseC(bijective_inverseC H). Proof. ir. app arrow_extensionality. ir.   set (g:= inverseC H). set (Ha:= (bijective_inverseC H)).   assert (bijectiveC g). uf g. am. red in H0. ee. red in H0. app H0.   uf g. rw inverseC_pra. rw inverseC_prb. tv. Qed. ```
Properties of the inverse of a bijection
``` Lemma inverse_bij_is_bij1:forall f,   bijective f -> bijective (inverse_fun f). Proof. ir. set (refl_equal (source f)). set (refl_equal (target f)).   assert(is_function f). fct_tac.   set (bcreate_bijective H0 e e0 H). set (inverseC_prc b).   rwi (bcreate_inv2 H0 e e0) e1. rw e1. app acreate_bijective.   app bijective_inverseC. Qed. Lemma inverse_bij_is_bij:forall f,   bijective f -> bijective (inverse_fun f). Proof. ir. assert (is_function f). fct_tac.   set (bijective_inv_function H). app inv_function_bijective.   rww inverse_fun_involutive. fct_tac. Qed. Lemma composable_f_inv:forall f,   bijective f -> composable f (inverse_fun f). Proof. ir. red.   assert (is_function (inverse_fun f)). app bijective_inv_function.   eee. fct_tac. uf inverse_fun. aw. Qed. Lemma composable_inv_f: forall f,   bijective f -> composable (inverse_fun f) f. Proof. ir. red.   assert (is_function (inverse_fun f)). app bijective_inv_function.   eee. fct_tac. uf inverse_fun. aw. Qed. Lemma bij_right_inverse:forall f,   bijective f -> compose f (inverse_fun f) = identity (target f). Proof. ir. set (refl_equal (source f)). set (refl_equal (target f)).   wr (identity_prop (target f)).   set (bij_is_function H).   wr (bcreate_inv2 i e e0). rw (inverseC_prc (bcreate_bijective i e e0 H)).   rw compose_acreate. rww bij_right_inverseC. aw. Qed. Lemma bij_left_inverse:forall f,   bijective f -> compose (inverse_fun f) f = identity (source f). Proof. ir. set (refl_equal (source f)). set (refl_equal (target f)).   set (bij_is_function H). wr (identity_prop (source f)).   wr (bcreate_inv2 i e e0). rw (inverseC_prc (bcreate_bijective i e e0 H)).   rw compose_acreate. rww bij_left_inverseC. aw. Qed. Lemma W_inverse: forall f x y,   bijective f -> inc x (target f) ->   (y = W x (inverse_fun f)) -> (x = W y f). Proof. ir. rw H1. transitivity (W x (identity (target f))). srw.   wr (bij_right_inverse H). aw. app composable_f_inv. Qed. Lemma W_inverse2: forall f x y,   bijective f -> inc y (source f) ->   (x = W y f) -> (y = W x (inverse_fun f)). Proof. ir. transitivity ( W y (identity (source f))). srw.   wr (bij_left_inverse H). aw. wrr H1. app composable_inv_f. Qed. Lemma W_inverse3: forall f x,   bijective f -> inc x (target f) -> inc (W x (inverse_fun f)) (source f). Proof. ir. assert (inc (W x (inverse_fun f)) (target (inverse_fun f))).   app inc_W_target. cp (inverse_bij_is_bij1 H). fct_tac. uf inverse_fun. aw.   ufi inverse_fun H1. awi H1. am. Qed. ```
Properties of direct and inverse images
``` Lemma sub_inv_im_source:forall f y,   is_function f -> sub y (target f) ->   sub (inv_image_by_graph (graph f) y) (source f). Proof. ir. red. ir. awi H1. nin H1. ee. graph_tac. Qed. Lemma direct_inv_im: forall f y,   is_function f -> sub y (target f) ->   sub (image_by_fun f (image_by_fun (inverse_fun f) y)) y. Proof. ir. red. ir. wri inv_image_by_fun_pr H1. ufi inv_image_by_fun H1.   rwi W_image H1. nin H1. nin H1. simpl in H1. awi H1. nin H1.   nin H1. red in H3. awi H3. wr H2. rww (W_pr H H3). am.   app sub_inv_im_source. Qed. Lemma direct_inv_im_surjective: forall f y,   surjective f -> sub y (target f) ->   (image_by_fun f (image_by_fun (inverse_fun f) y)) = y. Proof. ir. assert (Ha: is_function f). red in H; eee.   app extensionality. app direct_inv_im.   red. ir. wr inv_image_by_fun_pr. uf inv_image_by_fun.   rww W_image. nin (surjective_pr2 H (H0 _ H1)).   exists x0. ee. aw. ex_tac. wr H3. graph_tac. am.   app sub_inv_im_source. Qed. Lemma inverse_direct_image:forall f x,   is_function f -> sub x (source f) ->   sub x (image_by_fun (inverse_fun f) (image_by_fun f x)). Proof. ir. red. ir.   assert (inc (J x0 (W x0 f))(graph f)). graph_tac.   uf image_by_fun. aw. exists (W x0 f). split. aw. ex_tac. uf inverse_fun. aw. Qed. Lemma inverse_direct_image_inj:forall f x,   injective f -> sub x (source f) ->    x = (image_by_fun (inverse_fun f) (image_by_fun f x)). Proof. ir. app extensionality. app inverse_direct_image. fct_tac.   red. ir. nin H. wri inv_image_by_fun_pr H1. ufi inv_image_by_fun H1.   awi H1. nin H1. ee. awii H1. nin H1. nin H1. red in H3.   wri (W_pr H H3) H4.   wrr (H2 _ _ (H0 _ H1) (inc_pr1graph_source H H3) H4). Qed. ```

## EII-3-8 Retractions and sections

``` ```
Definition of left and right inverse
``` Definition is_left_inverse r f :=   composable r f & compose r f = identity (source f). Definition is_right_inverse s f :=   composable f s & compose f s = identity (target f). ```
Typechecking says that `r:b->a` and `s:b->a`
``` Definition is_left_inverseC (a b:Set) r (f:a->b) := composeC r f = identityC a. Definition is_right_inverseC (a b:Set) s (f:a->b):= composeC f s = identityC b. Lemma target_left_inverse: forall r f,   is_left_inverse r f -> target r = source f. Proof. ir. nin H. cp (f_equal target H0). ufi compose H1; ufi identity H1.   awii H1. Qed. Lemma source_right_inverse: forall s f,   is_right_inverse s f -> source s = target f. Proof. ir. nin H. cp (f_equal source H0).   ufi compose H1; ufi identity H1. awii H1. Qed. Lemma W_right_inverse: forall s f x,   is_right_inverse s f -> inc x (target f) -> W (W x s) f = x. Proof. ir. cp (source_right_inverse H).   red in H. ee. wrr compose_W. rw H2. srw. rww H1. Qed. Lemma W_left_inverse: forall r f x,   is_left_inverse r f -> inc x (source f) -> W (W x f) r = x. Proof. ir. cp (target_left_inverse H).   red in H. ee. wrr compose_W. rw H2. srw. Qed. Lemma w_right_inverse: forall (a b:Set) s (f:a->b) (x:b),   is_right_inverseC s f -> f (s x) = x. Proof. ir. red in H. transitivity (identityC b x). wrr H. tv. Qed. Lemma w_left_inverse: forall (a b:Set) r (f:a->b) (x:a),   is_left_inverseC r f -> r (f x) = x. Proof. ir. red in H. transitivity (identityC a x). wrr H. tv. Qed. ```
Proposition 8 concerns the next 4 theorems; it is the link between injectivity, surjectivity and existence of left and right inverse
``` Lemma inj_if_exists_left_invC: forall (a b:Set) (f:a-> b),   (exists r, is_left_inverseC r f) -> injectiveC f. Proof. ir. nin H. red. ee. ir. transitivity (x (f u)).   rww (w_left_inverse u H). rw H0. rww (w_left_inverse v H). Qed. Lemma surj_if_exists_right_invC: forall (a b:Set) (f:a->b),   (exists s, is_right_inverseC s f) -> surjectiveC f. Proof. ir. nin H. red. ir. exists (x u). rww (w_right_inverse u H). Qed. Theorem inj_if_exists_left_inv: forall f,   (exists r, is_left_inverse r f) -> injective f. Proof. ir. nin H. red. ee. nin H. red in H. ee. am.   ir. wr (W_left_inverse H H0). wr (W_left_inverse H H1). rww H2. Qed. Theorem surj_if_exists_right_inv: forall f,   (exists s, is_right_inverse s f) -> surjective f. Proof. ir. nin H. app surjective_pr6. nin H. red in H. ee. am.   ir. exists (W y x). rww W_right_inverse. wri (source_right_inverse H) H0.   nin H. red in H. ee. rw H3. fprops. tv. Qed. ```
Left inverse for an injective function `(f: a->b)`
``` Definition left_inverseC (a b:Set) (f: a->b)(H:nonemptyT a)   (v:b) := (chooseT (fun u:a => (~ (exists x:a, f x = v)) \/ (f u = v)) H). Lemma left_inverseC_pr:forall (a b:Set) (f: a->b) (H:nonemptyT a) (u:a),   f(left_inverseC f H (f u)) = f u. Proof. ir. uf left_inverseC.   set (p:=(fun u0 : a => (~ (exists x : a, f x = f u)) \/ f u0 = f u)).   set (y := chooseT p H). assert (p y). uf y. app chooseT_pr.   uf p. exists u. au. nin H0. nin H0. exists u. tv. am. Qed. Lemma left_inverse_comp_id: forall (a b:Set) (f:a->b) (H:nonemptyT a),   injectiveC f -> composeC (left_inverseC f H) f = identityC a. Proof. ir. app arrow_extensionality. ir. uf composeC. uf identityC.   app H0. app left_inverseC_pr. Qed. Lemma exists_left_inv_from_injC: forall (a b:Set) (f:a->b), nonemptyT a ->   injectiveC f -> exists r, is_left_inverseC r f. Proof. ir. exists (left_inverseC f H). red. app left_inverse_comp_id. Qed. ```
Right inverse for a surjective function `(f: a->b)`
``` Definition right_inverseC (a b:Set) (f: a->b) (H:surjectiveC f): b ->a.   ir. assert (nonemptyT a). nin (H H0). app nonemptyT_intro.   exact (chooseT (fun k:a => f k = H0) H1). Defined. Lemma right_inverse_pr: forall (a b:Set) (f: a->b) (H:surjectiveC f) (x:b),   f(right_inverseC H x) = x. Proof. ir. uf right_inverseC. app chooseT_pr. Qed. Lemma right_inverse_comp_id: forall (a b:Set) (f:a-> b) (H:surjectiveC f),   composeC f (right_inverseC H) = identityC b. Proof. ir. app arrow_extensionality. ir. uf composeC; uf identityC.   app right_inverse_pr. Qed. Lemma exists_right_inv_from_surjC: forall (a b:Set)(f:a-> b) (H:surjectiveC f),   exists s, is_right_inverseC s f. Proof. ir. exists (right_inverseC H). red. app right_inverse_comp_id. Qed. ```
Existence of left and right inverse for Bourbaki functions
``` Theorem exists_left_inv_from_inj: forall f,   injective f ->nonempty (source f) -> exists r, is_left_inverse r f. Proof. ir. set (inj_is_function H). set (bcreate1_injective (H:=i) H).   nin H0. nin (exists_left_inv_from_injC (inc_nonempty H0) i0).   exists (acreate x). red. ee. red. eee. aw.   red in H1. set (compose_acreate x (bcreate1 i)).   rwi bcreate_inv1 e. rw e. rww H1. Qed. Theorem exists_right_inv_from_surj: forall f,   surjective f -> exists s, is_right_inverse s f. Proof. ir. set (surj_is_function H).   set (bcreate1_surjective i H).   nin (exists_right_inv_from_surjC s).   exists (acreate x). red. ee. red. eee. aw.   set (compose_acreate (bcreate1 i) x).   rwi bcreate_inv1 e. rw e. rww H0. Qed. ```
If compositions in both order are the identity, then the functions are bijections
``` Lemma bijective_from_compose: forall g f,   composable g f -> composable f g -> compose g f = identity (source f)   -> compose f g = identity (source g)   -> (bijective f & bijective g & g = inverse_fun f). Proof. ir. assert (is_function f). fct_tac.   assert (is_function g). fct_tac.   assert (injective f). app inj_if_exists_left_inv. exists g. red. eee.   assert (injective g). app inj_if_exists_left_inv. exists f. red. eee.   assert (source f = target g). red in H0. ee. am. rwi H7 H1.   assert (source g = target f). red in H. ee. am. rwi H8 H2.   assert (bijective f).   red. ee. am. app surj_if_exists_right_inv. exists g. red. au.   ee. am. split. am. app surj_if_exists_right_inv. exists f. red. au.   sy. set (bijective_inv_function H9). app function_exten. sy; aw. aw.   ir. app W_pr. uf inverse_fun. aw. awi H10. set (identity_W H10). wri H2 e.   wri H8 H10. awi e. set (y:= W x g). wr e. uf y. graph_tac.   rw H7. fprops. am. am. Qed. ```
More links between left inverse and right inverse
``` Lemma right_inverse_from_leftC: forall (a b:Set) (r:b->a)(f:a->b),   is_left_inverseC r f -> is_right_inverseC f r. Proof. ir. tv. Qed. Lemma left_inverse_from_rightC: forall (a b:Set) (s:b->a)(f:a->b),   is_right_inverseC s f -> is_left_inverseC f s. Proof. ir. tv. Qed. Lemma left_inverse_surjectiveC: forall (a b:Set) (r:b->a)(f:a->b),   is_left_inverseC r f -> surjectiveC r. Proof. ir. ap surj_if_exists_right_invC. red in H. exists f. am. Qed. Lemma right_inverse_injectiveC: forall (a b:Set) (s:b->a)(f:a->b),   is_right_inverseC s f -> injectiveC s. Proof. ir. ap inj_if_exists_left_invC. red in H. exists f. am. Qed. Lemma section_uniqueC: forall (a b:Set) (f:a->b)(s:b->a)(s':b->a),   is_right_inverseC s f -> is_right_inverseC s' f ->   (forall x:a, (exists u:b, x = s u) = (exists u':b, x = s' u')) ->   s = s'. Proof. ir. app arrow_extensionality. ir.   cp (H1 (s a0)). assert (exists u' : b, s a0 = s' u'). wr H2. exists a0. tv.   nin H3. rw H3. assert (f (s a0) = f (s' x)). rww H3.   rwi (w_right_inverse a0 H) H4. rwi (w_right_inverse x H0) H4. rww H4. Qed. Lemma right_inverse_from_left: forall r f,   is_left_inverse r f -> is_right_inverse f r. Proof. ir. assert (Ha:=target_left_inverse H).   red in H. nin H. wri Ha H0. red. auto. Qed. Lemma left_inverse_from_right: forall s f,   is_right_inverse s f -> is_left_inverse f s. Proof. ir. assert (H0:=source_right_inverse H). red in H. wri H0 H.   ee. red. auto. Qed. Lemma left_inverse_surjective: forall f r,   is_left_inverse r f -> surjective r. Proof. ir. ap surj_if_exists_right_inv. exists f.   app right_inverse_from_left. Qed. Lemma right_inverse_injective: forall f s,   is_right_inverse s f -> injective s. Proof. ir. ap inj_if_exists_left_inv. exists f.   app left_inverse_from_right. Qed. Lemma section_unique: forall f s s',   is_right_inverse s f -> is_right_inverse s' f ->   range (graph s) = range (graph s') -> s = s'. Proof. ir. cp (source_right_inverse H). cp (source_right_inverse H0).   cp H. cp H0. red in H. red in H0. ee. red in H; red in H0; ee.   app function_exten. rww H3. wrr H11.   ir.   assert (inc (W x s) (range (graph s))). rw range_inc_rw. exists x. au.   am. rwi H2 H12. cp (W_right_inverse H4 H12).   rwi H1 H13. rwi range_inc_rw H13. nin H13. ee.   rwi H3 H13. cp (W_right_inverse H5 H13).   rw H15. wri H15 H16. rwi H14 H16. rww H16. am. Qed. ```
Theorem one is next 14 lemmas. It studies left and right invertibility of one of f g and the composition of f and g, given properties of the other objects.
``` Lemma composeC_inj: forall (a b c:Set) (f:a->b)(f':b->c),   injectiveC f-> injectiveC f' -> injectiveC (composeC f' f). Proof. ir. red. ir. app H. app H0. Qed. Lemma composeC_surj: forall (a b c:Set) (f:a->b)(f':b->c),   surjectiveC f-> surjectiveC f' -> surjectiveC (composeC f' f). Proof. ir. red. ir. nin (H0 u). nin (H x). exists x0. wr H1. wrr H2. Qed. Lemma composeC_bij: forall (a b c:Set) (f:a->b)(f':b->c),   bijectiveC f-> bijectiveC f' -> bijectiveC (composeC f' f). Proof. ir. red. red in H; red in H0. ee. app composeC_inj. app composeC_surj. Qed. Lemma left_inverse_composeC: forall (a b c:Set)   (f:a->b) (f':b->c)(r:b->a)(r':c->b),   is_left_inverseC r' f' -> is_left_inverseC r f ->   is_left_inverseC (composeC r r') (composeC f' f). Proof. ir. red. uf composeC. app arrow_extensionality. uf identityC. ir.   rw (w_left_inverse (f a0) H). rw (w_left_inverse a0 H0). tv. Qed. Lemma right_inverse_composeC:forall (a b c:Set)   (f:a->b) (f':b->c)(s:b->a)(s':c->b),   is_right_inverseC s' f' -> is_right_inverseC s f ->   is_right_inverseC (composeC s s') (composeC f' f). Proof. ir. red. uf composeC. app arrow_extensionality. ir. uf identityC.   rw (w_right_inverse (s' a0) H0). rw (w_right_inverse a0 H). tv. Qed. Lemma inj_right_composeC: forall (a b c:Set) (f:a->b) (f':b->c),   injectiveC (composeC f' f) -> injectiveC f. Proof. ir. red. ir. app H. simpl. uf composeC. ue. Qed. Lemma surj_left_composeC: forall (a b c:Set) (f:a->b) (f':b->c),   surjectiveC (composeC f' f) -> surjectiveC f'. Proof. ir. red. ir. nin (H u). exists (f x). am. Qed. Lemma surj_left_compose2C: forall (a b c:Set) (f:a->b) (f':b->c),   surjectiveC (composeC f' f) -> injectiveC f' -> surjectiveC f. Proof. ir. red. ir. nin (H (f' u)). exists x. app H0. Qed. Lemma inj_left_compose2C: forall (a b c:Set) (f:a->b) (f':b->c),   injectiveC (composeC f' f) -> surjectiveC f -> injectiveC f'. Proof. ir. red. ir. nin (H0 u). nin (H0 v). wri H2 H1. wri H3 H1.   assert (x = x0). app H. wr H2; wr H3; rww H4. Qed. Lemma left_inv_compose_rfC: forall (a b c:Set) (f:a->b) (f':b->c)(r'': c->a),   is_left_inverseC r'' (composeC f' f) ->   is_left_inverseC (composeC r'' f') f. Proof. ir. red. app arrow_extensionality. ir. ap (w_left_inverse a0 H). Qed. Lemma right_inv_compose_rfC : forall (a b c:Set) (f:a->b) (f':b->c)(s'': c->a),   is_right_inverseC s'' (composeC f' f) ->   is_right_inverseC (composeC f s'') f'. Proof. ir. red. app arrow_extensionality. ir. ap (w_right_inverse a0 H). Qed. Lemma left_inv_compose_rf2C: forall (a b c:Set) (f:a->b) (f':b->c)(r'': c->a),   is_left_inverseC r'' (composeC f' f) -> surjectiveC f ->   is_left_inverseC (composeC f r'') f'. Proof. ir. red. assert (bijectiveC f). red.   assert (injectiveC (composeC f' f)). ap inj_if_exists_left_invC.   exists r''. am. ee. ap (inj_right_composeC H1). am.   set (invf:= (inverseC H1)).   assert (f' = composeC f' (composeC f invf)). uf invf.   rw (bij_right_inverseC H1). rww compose_id_rightC.   app arrow_extensionality. uf identityC. ir. uf composeC.   assert (f' a0 = composeC f' (composeC f invf) a0). wr H2. tv.   ufi composeC H3. rw H3. ufi composeC H. rw (w_left_inverse (invf a0) H).   uf invf. app inverseC_prb. Qed. Lemma right_inv_compose_rf2C : forall (a b c:Set) (f:a->b) (f':b->c)(s'': c->a),   is_right_inverseC s'' (composeC f' f) -> injectiveC f'->   is_right_inverseC (composeC s'' f') f. Proof. ir. assert (bijectiveC f'). red. ee. am.   assert(surjectiveC (composeC f' f)). ap surj_if_exists_right_invC.   exists s''. am. app (surj_left_composeC H1).   set (invf:= inverseC H1).   assert (f = composeC (composeC invf f') f). uf invf.   rw (bij_left_inverseC H1). rww compose_id_leftC.   red. app arrow_extensionality. ir. uf identityC. rw H2.   uf composeC. ufi composeC H. rw (w_right_inverse (f' a0) H).   uf invf. app inverseC_pra. Qed. Theorem compose_injective: forall f f',   injective f-> injective f' -> composable f' f ->   injective (compose f' f). Proof. ir. red. ee. fct_tac. aw. ir. awi H4; try am.   red in H0; red in H; red in H1; ee.   app H8. app H7. ue. ue. Qed. Theorem compose_surjective: forall f f',   surjective f-> surjective f' -> composable f' f ->   surjective (compose f' f). Proof. ir. app surjective_pr6. fct_tac. aw. ir.   nin (surjective_pr2 H0 H2). ee. assert (inc x (target f)). red in H1; ee. ue.   nin (surjective_pr2 H H5). ee. ex_tac. aw. ue. Qed. Lemma compose_bijective: forall f f',   bijective f-> bijective f' -> composable f' f ->   bijective (compose f' f). Proof. ir. red. red in H; red in H0. ee.   app compose_injective. app compose_surjective. Qed. Lemma bij_right_compose: forall f f',   composable f' f-> bijective (compose f' f) -> bijective f' ->bijective f. Proof. ir. set (g:= inverse_fun f'). assert (bijective g). uf g.   app inverse_bij_is_bij.   assert (bijective (compose g (compose f' f))). app compose_bijective.   uf g; red; eee; aw; fct_tac.   wri compose_assoc H3. ufi g H3. rwi bij_left_inverse H3. red in H. ee.   rwi H5 H3. rwi compose_identity_left H3. am. fct_tac. am.   uf g. red;eee; aw;fct_tac. am. Qed. Lemma bij_left_compose: forall f f',   composable f' f-> bijective (compose f' f) -> bijective f ->bijective f'. Proof. ir. set (g:= inverse_fun f). assert (bijective g). uf g.   app inverse_bij_is_bij.   assert (bijective (compose (compose f' f) g)). app compose_bijective.   red. aw. eee; try fct_tac. uf g; aw.   rwi compose_assoc H3. ufi g H3. rwi bij_right_inverse H3. red in H. ee.   wri H5 H3. rwi compose_identity_right H3. am. fct_tac. am. am.   red. eee; try fct_tac. uf g; aw. Qed. Lemma left_inverse_composable: forall f f' r r', composable f' f ->   is_left_inverse r' f' -> is_left_inverse r f -> composable r r'. Proof. ir. cp (target_left_inverse H0). red in H0; red in H1. ee.   red in H0; red in H1. ee. red. eee. red in H. ee. ue. Qed. Lemma right_inverse_composable: forall f f' s s', composable f' f ->   is_right_inverse s' f' -> is_right_inverse s f -> composable s s'. Proof. ir. cp (source_right_inverse H1). red in H0; red in H1. ee.   red in H0; red in H1. ee. red. eee. red in H. ee. wrr H10. Qed. Theorem left_inverse_compose: forall f f' r r', composable f' f ->   is_left_inverse r' f' -> is_left_inverse r f ->   is_left_inverse (compose r r') (compose f' f). Proof. ir. cp (left_inverse_composable H H0 H1).   cp (target_left_inverse H0).   red in H0; red in H1; ee. red. ee. red. red in H0; ee; aw; fct_tac.   aw. wrr compose_assoc. rw (@compose_assoc r r' f'). rw H5.   assert (source f' = source r). wr H3. red in H2; ee; sy;am. rw H6.   rww compose_id_right. fct_tac. am. am. red. red in H0; ee; aw; fct_tac. Qed. Theorem right_inverse_compose: forall f f' s s', composable f' f ->   is_right_inverse s' f' -> is_right_inverse s f ->   is_right_inverse (compose s s') (compose f' f). Proof. ir. cp (right_inverse_composable H H0 H1).   cp (source_right_inverse H1). red in H0; red in H1; ee.   red. ee. red. ee. fct_tac. fct_tac. aw. red in H1; ee; am.   rww compose_assoc. wr (@compose_assoc f s s'). rw H4.   assert (target f = target s'). wr H3. red in H2; eee. rw H6.   rww compose_id_left. aw. fct_tac. am. am. red in H1. red. eee; aw; fct_tac. Qed. Theorem inj_right_compose: forall f f',   composable f' f-> injective (compose f' f) -> injective f. Proof. ir. red. ee. red in H; ee; am. ir. red in H0. ee. awi H4.   app H4. aw. ue. Qed. Theorem surj_left_compose: forall f f',   composable f' f-> surjective (compose f' f) -> surjective f'. Proof. ir. app surjective_pr6. red in H;ee;am. ir.   assert (target f' = target(compose f' f)). aw.   rwi H2 H1. nin (surjective_pr2 H0 H1). ee. awi H3.   awi H4. exists (W x f). ee. red in H;ee. ue. am. am. am. Qed. Theorem surj_left_compose2: forall f f',   composable f' f-> surjective (compose f' f) -> injective f' -> surjective f. Proof. ir. app surjective_pr6. red in H;eee. ir. red in H. ee.   assert (inc (W y f') (target (compose f' f))). aw. nin H1. wri H4 H2.   fprops. nin (surjective_pr2 H0 H5). ee. awi H6.   awi H7. exists x. ee. am. red in H1. ee. rwi H4 H8. app H8.   fprops. red; au. am. Qed. Theorem inj_left_compose2: forall f f',   composable f' f-> injective (compose f' f) -> surjective f -> injective f'. Proof. red. ir. ee. red in H; eee. ir.   assert (source f' = target f). red in H; eee.   rwi H5 H2. nin (surjective_pr2 H1 H2). ee.   rwi H5 H3. nin (surjective_pr2 H1 H3). ee.   red in H0; ee. assert (x0=x1). app H10.   aw. aw. aw. rw H7. rww H9. wr H7; wr H9. ue. Qed. Theorem left_inv_compose_rf: forall f f' r'',   composable f' f-> is_left_inverse r'' (compose f' f) ->   is_left_inverse (compose r'' f') f. Proof. ir. cp (target_left_inverse H0). red in H0. ee. cp H.   red in H; red in H0. ee. awi H1. awi H5. awi H2.   assert(composable r'' f'). red; ee; am.   red. ee. red. eee. fct_tac. aw. rww compose_assoc. Qed. Theorem right_inv_compose_rf : forall f f' s'',   composable f' f-> is_right_inverse s'' (compose f' f) ->   is_right_inverse (compose f s'') f'. Proof. ir. cp (source_right_inverse H0). nin H0. cp H. red in H0; red in H;ee.   awi H2; awi H1. awi H5.   assert (composable f s''). red. ee; am.   split. red. eee. fct_tac. aw. wrr compose_assoc. Qed. Theorem left_inv_compose_rf2: forall f f' r'',   composable f' f-> is_left_inverse r'' (compose f' f) -> surjective f ->   is_left_inverse (compose f r'') f'. Proof. ir. assert (bijective f). red.   assert (injective (compose f' f)). ap inj_if_exists_left_inv. exists r''. am.   ee. ap (inj_right_compose H H2). am.   cp (target_left_inverse H0). red in H0. ee. awi H4. awi H3.   assert (composable f r''). red. ee. fct_tac. fct_tac. sy; am.   assert(is_function (compose f r'')). fct_tac.   red. ee. red. ee. am. fct_tac. aw. red in H0; ee. awi H8. exact H8.   set (invf:= (inverse_fun f)).   assert(is_function invf). uf invf. app bijective_inv_function.   assert (source f = target invf). uf invf; aw.   assert (f' = compose f' (compose f invf)). uf invf.   rw (bij_right_inverse H2).   red in H; ee. wr H10. rww compose_id_right. wri compose_assoc H9. rw H9.   rw compose_assoc. wrr (@compose_assoc r'' (compose f' f) invf). rw H4.   aw. assert (source f = target invf). uf invf; aw. rw H10.   rww compose_id_left.   uf invf. rww bij_right_inverse. aw. red. split. fct_tac. split. am. aw. am.   wr H9. red. red in H0. eee. fct_tac. aw. aw. am. uf invf.   app composable_f_inv. Qed. Theorem right_inv_compose_rf2 : forall f f' s'',   composable f' f-> is_right_inverse s'' (compose f' f) -> injective f'->   is_right_inverse (compose s'' f') f. Proof. ir. assert (bijective f'). red. ee. am.   assert(surjective (compose f' f)). ap surj_if_exists_right_inv. exists s''.   am. app (surj_left_compose H H2).   cp (source_right_inverse H0). awi H3. red in H0. ee.   assert (composable s'' f'). red. ee. fct_tac. fct_tac. am.   assert(is_function (compose s'' f')). fct_tac.   assert(composable f (compose s'' f')). red in H0. ee. red. ee.   fct_tac. am. aw. awi H8. exact H8. cp (bijective_inv_function H2).   set (invf:= inverse_fun f').   assert (f = compose invf (compose f' f)). uf invf.   wrr compose_assoc. rw (bij_left_inverse H2). red in H; ee. rw H10.   rww compose_id_left. app composable_inv_f.   split. am. rw H9. rw compose_assoc.   wr (@compose_assoc (compose f' f) s'' f'). rw H4. aw.   rw compose_id_left. uf invf. rww (bij_left_inverse H2). aw. fct_tac. am.   am. red. uf invf. eee. fct_tac. aw. red. red in H0; eee. aw. Qed. ```
Properties of equipotency
``` Lemma equipotent_reflexive: forall x, equipotent x x. Proof. ir. rw equipotentC. exists (identityC x). app identityC_bijective. Qed. Lemma equipotent_symmetric: forall a b,   equipotent a b -> equipotent b a. Proof. ir. rwi equipotentC H. nin H. rw equipotentC. exists (inverseC H).   app bijective_inverseC. Qed. Lemma equipotent_transitive: forall a b c,   equipotent a b -> equipotent b c -> equipotent a c. Proof. ir. rwi equipotentC H;rwi equipotentC H0. nin H; nin H0.   rw equipotentC. exists (composeC x0 x). app composeC_bij. Qed. Hint Resolve equipotent_reflexive: fprops. ```
Proposition 9 is the next 6 lemmas (each in 2 variants). Given f and g, when does there exists h such that the composition with f (in any order) is g
``` Lemma exists_left_composableC: forall (a b c:Set) (f:a->b)(g:a->c),   surjectiveC g ->   (exists h, composeC h g = f) =   (forall (x y:a), g x = g y -> f x = f y). Proof. ir. app iff_eq. ir. nin H0. wr H0. uf composeC. rww H1. ir.   pose (exists_right_inv_from_surjC H). nin e.   exists (composeC f x). app arrow_extensionality. ir. uf composeC.   app H0. rw (w_right_inverse (g a0) H1). tv. Qed. Theorem exists_left_composable: forall f g,   is_function f -> surjective g -> source f = source g ->   (exists h, composable h g & compose h g = f) =   (forall x y, inc x (source g) -> inc y (source g) ->     W x g = W y g -> W x f = W y f). Proof. ir. app iff_eq. ir. nin H2. ee. wr H6. aw. rww H5.   ir. assert (Ha: is_function g). fct_tac. cp (bcreate1_surjective Ha H0).   set (bf:=bcreate H H1 (refl_equal (target f))).   assert (exists h : target g -> (target f), composeC h (bcreate1 Ha) = bf).   rw (exists_left_composableC bf H3).   uf bf. ir. app R_inj. do 2 rw prop_bcreate2.   app H2. app R_inc. app R_inc. do 2 wr (prop_bcreate1 Ha). rww H4.   nin H4. exists (acreate x). ee. red. ee. fprops. am. aw.   assert (acreate (composeC x (bcreate1 Ha)) = acreate bf). rww H4.   wri compose_acreate H5. rwi (bcreate_inv1 Ha) H5. rw H5.   uf bf. rww bcreate_inv2. Qed. Lemma exists_left_composable_auxC: forall (a b c:Set) (f:a->b) (g:a-> c) s h,   surjectiveC g -> is_right_inverseC s g ->   composeC h g = f -> h = composeC f s. Proof. ir. wr H1. rw compositionC_associative. red in H0. rw H0. sy.   app compose_id_rightC. Qed. Theorem exists_left_composable_aux: forall f g s h ,   is_function f -> surjective g -> source f = source g ->   is_right_inverse s g ->   composable h g -> compose h g = f -> h = compose f s. Proof. ir. wr H4. rw compose_assoc. red in H2. ee. rw H5.   assert (target g = source h). sy. red in H3; eee. rw H6. sy.   app compose_id_right. fct_tac. am. red in H2; eee. Qed. Lemma exists_unique_left_composableC: forall (a b c:Set) (f:a->b)(g:a->c) h h',   surjectiveC g -> composeC h g = f -> composeC h' g = f ->   h = h'. Proof. ir. cp (exists_right_inv_from_surjC H). nin H2.   set (exists_left_composable_auxC H H2 H1).   set (exists_left_composable_auxC H H2 H0).   rw e; rw e0. tv. Qed. Theorem exists_unique_left_composable: forall f g h h',   is_function f -> surjective g -> source f = source g ->   composable h g -> compose h g = f ->   composable h' g -> compose h' g = f -> h = h'. Proof. ir. cp (exists_right_inv_from_surj H0). nin H6.   pose (exists_left_composable_aux H H0 H1 H6 H2 H3).   pose (exists_left_composable_aux H H0 H1 H6 H4 H5).   rw e; rw e0. tv. Qed. Lemma left_composable_valueC: forall (a b c:Set) (f:a->b)(g:a->c) s h,   surjectiveC g -> (forall (x y:a), g x = g y -> f x = f y) ->   is_right_inverseC s g -> h = composeC f s ->   composeC h g = f. Proof. ir. app arrow_extensionality. ir. rw H2. uf composeC. app H0.   rw (w_right_inverse (g a0) H1). tv. Qed. Theorem left_composable_value: forall f g s h,   is_function f -> surjective g -> source f = source g ->   (forall x y, inc x (source g) -> inc y (source g) ->     W x g = W y g -> W x f = W y f) ->   is_right_inverse s g -> h = compose f s-> compose h g = f. Proof. ir. red in H0; ee.   cp (source_right_inverse H3). red in H3. ee. rw H4.   assert (composable f s). red. ee. am. fct_tac. red in H3; ee. rww H1.   assert (composable (compose f s) g). red. ee;aw;fct_tac.   app function_exten. fct_tac. sy; aw. aw. aw. ir. aw. app H2.   red in H3; ee. rw H12. app inc_W_target. rw H6. fprops.   set (w:= (W x g)). wr compose_W. rw H7. srw. uf w.   fprops. am. uf w. ue. ue. Qed. Lemma exists_right_composable_auxC: forall (a b c:Set) (f:a->b) (g:c->b) h r,   injectiveC g -> is_left_inverseC r g -> composeC g h = f   -> h = composeC r f. Proof. ir. wr H1. wr compositionC_associative. rw H0. rww compose_id_leftC. Qed. Theorem exists_right_composable_aux: forall f g h r,   is_function f -> injective g -> target f = target g ->   is_left_inverse r g -> composable g h -> compose g h = f   -> h = compose r f. Proof. ir. wr H4. wr compose_assoc. red in H2. ee. rw H5.   red in H3; ee. rw H7. rww compose_id_left. red in H2; eee. am. Qed. Lemma exists_right_composable_uniqueC: forall (a b c:Set)(f:a->b) (g:c->b) h h',   injectiveC g -> composeC g h = f -> composeC g h' = f -> h = h'. Proof. ir. app arrow_extensionality. ir.   cp (exists_left_inv_from_injC (nonemptyT_intro (h a0)) H). nin H2.   assert (x (composeC g h a0) = x (composeC g h' a0)). rw H0; rw H1; tv.   ufi composeC H3. rwi (w_left_inverse (h a0) H2) H3.   rwi (w_left_inverse (h' a0) H2) H3. am. Qed. Theorem exists_right_composable_unique: forall f g h h',   is_function f -> injective g -> target f = target g ->   composable g h -> compose g h = f ->   composable g h' -> compose g h' = f -> h = h'. Proof. ir. nin (emptyset_dichot (source g)).   ir. app function_exten. red in H2; eee. red in H4; eee.   transitivity (source f). wr H3. aw. wr H5. aw. red in H2; ee. wr H8.   red in H4; ee. am. ir. red in H2; ee. assert (inc (W x h) (target h)).   fprops. wri H9 H10. rwi H6 H10. nin H10. elim x0.   cp (exists_left_inv_from_inj H0 H6). nin H7.   pose (exists_right_composable_aux H H0 H1 H7 H2 H3).   pose (exists_right_composable_aux H H0 H1 H7 H4 H5). rw e; rw e0; tv. Qed. Lemma exists_right_composableC: forall (a b c:Set) (f:a->b) (g:c->b),   injectiveC g ->   (exists h, composeC g h = f) = (forall u, exists v, g v = f u). Proof. ir. app iff_eq. ir. nin H0. wr H0. uf composeC. exists (x u). tv.   ir. nin (emptyset_dichot c).   assert(a = emptyset). ap is_emptyset. red. ir.   nin (H0 (Bo H2)). clear H3. rwi H1 x. elim x.   symmetry in H1; symmetry in H2. cp empty_function_function.   assert (source empty_function = a). uf empty_function. aw.   assert (target empty_function = c). uf empty_function. aw.   set (h:=bcreate H3 H4 H5). exists h. app arrow_extensionality. ir.   assert False. wri H2 a0. elim a0. elim H6. nin H1.   nin (exists_left_inv_from_injC (inc_nonempty H1) H).   exists (composeC x f). app arrow_extensionality. ir. uf composeC.   nin (H0 a0). wr H3. rww (w_left_inverse x0 H2). Qed. Theorem exists_right_composable: forall f g,   is_function f -> injective g -> target f = target g ->   (exists h, composable g h & compose g h = f) =   (sub (range (graph f)) (range (graph g))). Proof. ir. assert (Ha:is_function g). fct_tac.   app iff_eq. ir. nin H2. nin H2. assert (source x = source f). wr H3. aw.   red. ir. awi H5. nin H5. cp (inc_pr1graph_source H H5). wri H4 H6.   aw. exists (W x1 x). wr (W_pr H H5). wr H3. aw. graph_tac.   red in H2. ee. rw H8. fprops. fprops. fprops.   ir. nin (emptyset_dichot(source g)). nin (emptyset_dichot(source f)).   exists (empty_function).   assert (composable g empty_function). red. ee. am.   app empty_function_function. uf empty_function. aw. ee. am.   app function_exten. fct_tac.   sy;aw. uf empty_function. aw. sy;aw. aw. ir.   ufi empty_function H6. awi H6. elim (emptyset_pr H6).   nin H. nin H5. rwi H6 H4. nin H4. set (gf:=graph f) in H4. awi H4. nin H4.   assert (inc x (range (graph g))). app H2. aw. exists y.   am. fprops. awi H7. nin H7. cp (inc_pr1graph_source Ha H7).   rwi H3 H8. elim (emptyset_pr H8). fprops. fprops.   nin (exists_left_inv_from_inj H0 H3).   cp (target_left_inverse H4). red in H4; ee.   assert (composable x f). red. ee. fct_tac. am. ue. red in H4; eee.   assert(is_function (compose x f)). fct_tac.   assert (composable g (compose x f)). red. aw. auto.   exists (compose x f). ee. am. ap function_exten. fct_tac.   am. aw. sy;aw. ir. awi H10. aw. wri (f_domain_graph H) H10.   set (gf:= graph f) in H10.   awi H10. nin H10. rw (W_pr H H10).   assert (inc x1 (range (graph g))). app H2. aw. exists x0. am. fprops.   awi H11. nin H11. assert (inc x2 (source g)). graph_tac.   wr (W_pr Ha H11). assert (W x2 (compose x g) = x2). rww H6.   srw. awi H13. ue. am. am. fprops. uf gf. fprops. Qed. Lemma right_composable_valueC: forall (a b c:Set) (f:a->b) (g:c->b) r h,   injectiveC g -> is_left_inverseC r g -> (forall u, exists v, g v = f u) ->   h = composeC r f -> composeC g h = f. Proof. ir. rw H2. app arrow_extensionality. ir. nin (H1 a0).   uf composeC. wr H3. rww (w_left_inverse x H0). Qed. Theorem right_composable_value: forall f g r h,   is_function f -> injective g -> target g = target f ->   is_left_inverse r g ->   (sub (range (graph f)) (range (graph g))) ->   h = compose r f ->   compose g h = f. Proof. ir. rw H4. cp (target_left_inverse H2). red in H2; ee.   assert (composable r f). red. ee. fct_tac. am. red in H2; ee. rww H8.   assert (composable g (compose r f)). red. eee. fct_tac. fct_tac. sy;aw.   assert (composable g r). red. eee; fct_tac.   app function_exten. fct_tac. aw. aw. aw. ir.   assert (inc (W x f) (range (graph g))).   app H3. rw range_inc_rw. exists x. au.   fct_tac. rwi range_inc_rw H11. nin H11. ee. aw. rw H12.   wr compose_W. wr compose_W.   rww compose_assoc. rw H6. aw. srw. red. ee.   red in H0; ee; am. fprops. aw.   red. red in H2; eee; try fct_tac. aw. ue. am. am.   red in H2; ee. rw H14. fprops. fct_tac. Qed. ```

## EII-3-9 Functions of two arguments

``` ```
Given a function f with two arguments and one argument, we obtain a function of one argument
``` Definition partial_fun2 f y :=   BL(fun x=> W (J x y) f) (im_singleton (inverse_graph (source f)) y) (target f). Definition partial_fun1 f x :=   BL(fun y=> W (J x y) f)(im_singleton (source f) x) (target f). Lemma partial_fun1_axioms: forall f x, is_function f -> is_graph(source f) ->   transf_axioms (fun y=> W (J x y) f)(im_singleton (source f) x) (target f). Proof. ir. red. ir. rwi im_singleton_pr H1. fprops. Qed. Lemma partial_fun1_function: forall f x, is_function f -> is_graph(source f) ->   is_function (partial_fun1 f x). Proof. ir. uf partial_fun1. app bl_function. app partial_fun1_axioms. Qed. Lemma partial_fun1_W: forall f x y, is_function f -> is_graph(source f) ->   inc (J x y) (source f) -> W y (partial_fun1 f x) = W (J x y) f. Proof. ir. uf partial_fun1. aw. app partial_fun1_axioms. Qed. Lemma partial_fun2_axioms: forall f y, is_function f -> is_graph(source f) ->   transf_axioms (fun x=> W (J x y) f)(im_singleton (inverse_graph (source f)) y)   (target f). Proof. ir. red. ir. rwi im_singleton_pr H1. awi H1. fprops. Qed. Lemma partial_fun2_function: forall f y, is_function f -> is_graph(source f) ->   is_function (partial_fun2 f y). Proof. ir. uf partial_fun2. app bl_function. ap partial_fun2_axioms. am. am. Qed. Lemma partial_fun2_W: forall f x y, is_function f -> is_graph(source f) ->   inc (J x y) (source f) -> W x (partial_fun2 f y) = W (J x y) f. Proof. ir. uf partial_fun2. aw. app partial_fun2_axioms. aw. Qed. ```
Product of two functions
``` Definition ext_to_prod u v :=   BL(fun z=> J (W (P z) u)(W (Q z) v))   (product (source u)(source v))   (product (target u)(target v)). Lemma ext_to_prod_function: forall u v,   is_function u -> is_function v ->   is_function (ext_to_prod u v). Proof. ir. uf ext_to_prod. app bl_function. red. ir. awi H1. ee.   aw. eee. Qed. Hint Resolve ext_to_prod_function: fprops. Lemma ext_to_prod_W: forall u v a b,   is_function u -> is_function v-> inc a (source u) -> inc b (source v)->   W (J a b) (ext_to_prod u v) = J (W a u) (W b v). Proof. ir. uf ext_to_prod. aw.   red. ir. awi H3. ee. aw. eee. eee. Qed. Lemma ext_to_prod_W2: forall u v c,   is_function u -> is_function v->   inc c (product (source u)(source v)) ->   W c (ext_to_prod u v) = J (W (P c) u) (W (Q c) v). Proof. ir. awi H1. ee.   assert (J (P c) (Q c) =c). aw. wr H4. rww ext_to_prod_W. aw. Qed. Lemma ext_to_prod_range: forall u v,   is_function u -> is_function v->   range (graph (ext_to_prod u v)) =     product (range (graph u))(range (graph v)). Proof. ir. assert (is_function (ext_to_prod u v)). fprops.   set_extens. awi H2. nin H2. cp (W_pr H1 H2).   assert (inc x0 (source (ext_to_prod u v))). graph_tac. cp H4.   ufi ext_to_prod H4. awi H4. aw.   rwii ext_to_prod_W2 H3. aw. ee. wr H3; fprops.   exists (P x0). wr H3. aw. graph_tac.   exists (Q x0). wr H3. aw. graph_tac. aw.   fprops. fprops. fprops.   awi H2. ee. nin H3; nin H4. aw.   exists (J x0 x1). uf ext_to_prod. uf BL. aw. uf L. aw.   exists (J x0 x1). split. aw. ee. fprops. graph_tac. graph_tac.   aw. app uneq2. rw (W_pr H H3). rw (W_pr H0 H4). aw. fprops. fprops. fprops. Qed. Lemma ext_to_prod_propP: forall a a' (x: product a a'), inc (P (Ro x)) a. Proof. ir. assert (inc (Ro x) (product a a')). app R_inc. awi H. int. Qed. Lemma ext_to_prod_propQ: forall a a' (x: product a a'), inc (Q (Ro x)) a'. Proof. ir. assert (inc (Ro x) (product a a')). app R_inc. awi H. int. Qed. Lemma ext_to_prod_propJ: forall (b b':Set) (x:b)(x':b'),   inc (J (Ro x)(Ro x')) (product b b'). Proof. ir. aw. ee. fprops. app R_inc. app R_inc. Qed. Definition pr1C a b:= fun x:product a b => Bo(ext_to_prod_propP x). Definition pr2C a b:= fun x:product a b => Bo(ext_to_prod_propQ x). Definition pairC (a b:Set) := fun (x:a)(y:b) => Bo(ext_to_prod_propJ x y). Definition ext_to_prodC (a b a' b':Set) (u:a->a')(v:b->b') :=   fun x => pairC (u (pr1C x)) (v (pr2C x)). Lemma prC_prop: forall (a b:Set) (x:product a b),   Ro x = J (Ro (pr1C x)) (Ro (pr2C x)). Proof. ir. assert (inc (Ro x) (product a b)). app R_inc. awi H.   ee. uf pr1C. rw B_eq. uf pr2C. rw B_eq. aw. Qed. Lemma pr1C_prop: forall (a b:Set) (x:product a b),   Ro (pr1C x) = P (Ro x). Proof. ir. rw (prC_prop x). aw. Qed. Lemma pr2C_prop: forall (a b:Set) (x:product a b),   Ro (pr2C x) = Q (Ro x). Proof. ir. rw (prC_prop x). aw. Qed. Lemma prJ_prop: forall (a b:Set) (x:a)(y:b),   Ro(pairC x y) = J (Ro x) (Ro y). Proof. ir. uf pairC. rw B_eq. tv. Qed. Lemma prJ_recov: forall (a b:Set) (x:product a b),   pairC (pr1C x) (pr2C x) = x. Proof. ir. app R_inj. rw prJ_prop. rw pr1C_prop. rw pr2C_prop. aw.   assert (inc (Ro x) (product a b)). app R_inc. awi H. eee. Qed. Lemma ext_to_prod_prop:   forall (a b a' b':Set) (u:a->a')(v:b->b') (x:a)(x':b),   J(Ro (u x)) (Ro (v x')) = Ro(ext_to_prodC u v (pairC x x')). Proof. ir. uf ext_to_prodC. rw prJ_prop.   assert (x = (pr1C (pairC x x'))). app R_inj. rw pr1C_prop.   rw prJ_prop. aw. wr H.   assert (x' = (pr2C (pairC x x'))). app R_inj. rw pr2C_prop.   rw prJ_prop. aw. wr H0. tv. Qed. ```
If the two functions are a injective, surjective, bijective, so is the product. The inverse of the prodiuct is trivial
``` Lemma ext_to_prod_injective: forall u v,   injective u -> injective v-> injective (ext_to_prod u v). Proof. ir. nin H. nin H0.   red. ee. fprops. ir. ufi ext_to_prod H3. awi H3.   ufi ext_to_prod H4. awi H4.   rwii ext_to_prod_W2 H5. rwii ext_to_prod_W2 H5. awi H3. awi H4. ee.   app pair_extensionality. app H1. inter2tac. app H2. inter2tac. aw. aw. Qed. Lemma ext_to_prod_surjective: forall u v,   surjective u -> surjective v-> surjective (ext_to_prod u v). Proof. ir. assert (Ha:is_function u). red in H; eee.   assert (Hb:is_function v). red in H0; eee.   app surjective_pr6. fprops. ir.   ufi ext_to_prod H1. awi H1. ee. cp (surjective_pr2 H H2).   cp (surjective_pr2 H0 H3).   nin H4; nin H5;ee. exists (J x x0). ee. uf ext_to_prod. aw. ee. fprops.   aw. aw.   rww ext_to_prod_W. assert(J (P y) (Q y) = y). aw. wr H8. wr H7; wr H6. tv. Qed. Lemma ext_to_prod_bijective: forall u v,   bijective u -> bijective v-> bijective (ext_to_prod u v). Proof. uf bijective. ir. ee. app ext_to_prod_injective.   app ext_to_prod_surjective. Qed. Lemma ext_to_prod_inverse: forall u v,   bijective u -> bijective v->   inverse_fun (ext_to_prod u v) =   ext_to_prod (inverse_fun u)(inverse_fun v). Proof. ir.   assert (Ha:bijective (ext_to_prod u v)). app ext_to_prod_bijective.   assert (Hb:is_function (inverse_fun u)). app bijective_inv_function.   assert (Hc:is_function (inverse_fun v)). app bijective_inv_function.   ap function_exten. app bijective_inv_function.   fprops. uf ext_to_prod. aw. uf ext_to_prod. aw.   aw. ir. ufi ext_to_prod H1. awi H1.   ee. set (Py := W (P x) (inverse_fun u)).   assert (P x = W Py u). app W_inverse.   set (Qy := W (Q x) (inverse_fun v)).   assert (Q x = W Qy v). app W_inverse.   rww ext_to_prod_W2. fold Py. fold Qy.   assert (inc Py (target (inverse_fun u))). uf Py. app inc_W_target. aw.   assert (inc Qy (target (inverse_fun v))). uf Qy. app inc_W_target. aw.   assert (inc (Q x) (source (inverse_fun v))). aw. fprops.   sy. ap W_inverse2. am. awi H6; awi H7; uf ext_to_prod. aw. eee.   awi H6. awi H7. rw ext_to_prod_W. wr H4; wr H5. sy. aw.   red in H;ee; red in H; ee;am. red in H0;ee; red in H0; eee. am. am. bw.   aw. eee. Qed. ```
Composition of products
``` Lemma composable_ext_to_prod2: forall u v u' v',   composable u' u -> composable v' v ->   composable (ext_to_prod u' v') (ext_to_prod u v). Proof. ir. red in H; red in H0. ee. red. ee.   fprops. fprops. uf ext_to_prod. aw.   rw H4; rw H2. tv. Qed. Lemma compose_ext_to_prod2: forall u v u' v',   composable u' u -> composable v' v ->   compose (ext_to_prod u' v') (ext_to_prod u v) =   ext_to_prod (compose u' u)(compose v' v). Proof. ir. assert (composable (ext_to_prod u' v') (ext_to_prod u v)).   app composable_ext_to_prod2.   assert (is_function (compose u' u)). fct_tac.   assert (is_function (compose v' v)). fct_tac. red in H; red in H0; ee.   ap function_exten. fct_tac.   fprops. uf ext_to_prod. aw. uf ext_to_prod. aw. aw.   ir. cp H8. ufi ext_to_prod H9. awi H9. ee.   aw. rww ext_to_prod_W2. rww ext_to_prod_W2. rww ext_to_prod_W2. aw.   red. au. red; au. aw. eee. aw. eee.   assert (product (source u') (source v')= target(ext_to_prod u v)).   rw H7; rw H5. uf ext_to_prod. aw. rw H12. app inc_W_target.   fprops. Qed. Lemma injective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),   injectiveC u -> injectiveC v-> injectiveC (ext_to_prodC u v). Proof. ir. red. ir. assert (pairC (pr1C u0) (pr2C u0) = u0).   rw prJ_recov. tv. assert (pairC (pr1C v0) (pr2C v0) = v0).   rw prJ_recov. tv.   assert (Ro (ext_to_prodC u v u0) = Ro (ext_to_prodC u v v0)).   rw H1. tv. wri H2 H4. wri ext_to_prod_prop H4.   wri H3 H4. wri ext_to_prod_prop H4.   assert(pr1C u0 = pr1C v0). app H. app R_inj. inter2tac.   wri H5 H3. assert(pr2C u0 = pr2C v0). app H0. app R_inj.   inter2tac. wri H6 H3. wr H2; wr H3. tv. Qed. Lemma surjective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),   surjectiveC u -> surjectiveC v-> surjectiveC (ext_to_prodC u v). Proof. ir. red. ir. wr (prJ_recov u0).   nin (H (pr1C u0)). nin (H0 (pr2C u0)).   exists (pairC x x0). app R_inj. wr ext_to_prod_prop.   rw prJ_recov. rw H1; rw H2. rw pr1C_prop. rw pr2C_prop. aw.   assert (inc (Ro u0) (product a' b')). app R_inc. awi H3. ee. am. Qed. Lemma bijective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),   bijectiveC u -> bijectiveC v-> bijectiveC (ext_to_prodC u v). Proof. uf bijectiveC. ir. ee. app injective_ext_to_prod2C.   app surjective_ext_to_prod2C. Qed. Lemma compose_ext_to_prod2C: forall (a b c a' b' c':Set) (u:b-> c)(v:a->b)   (u':b'-> c')(v':a'->b'),   composeC (ext_to_prodC u u') (ext_to_prodC v v') =   ext_to_prodC (composeC u v)(composeC u' v'). Proof. ir. uf composeC. app arrow_extensionality. ir. app R_inj.   wr (prJ_recov a0). wr ext_to_prod_prop.   cp (ext_to_prod_prop v v' (pr1C a0) (pr2C a0)). wri prJ_prop H.   cp (R_inj H). wr H0. wr ext_to_prod_prop. tv. Qed. Lemma inverse_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b')   (Hu: bijectiveC u)(Hv:bijectiveC v),   inverseC (bijective_ext_to_prod2C Hu Hv)=   ext_to_prodC (inverseC Hu)(inverseC Hv). Proof. ir. app arrow_extensionality. ir.   assert (a0 = ext_to_prodC u v (ext_to_prodC (inverseC Hu) (inverseC Hv) a0)).   cp ( compose_ext_to_prod2C u (inverseC Hu) v(inverseC Hv)).   assert (composeC (ext_to_prodC u v)     (ext_to_prodC (inverseC Hu) (inverseC Hv)) a0 =       ext_to_prodC (composeC u (inverseC Hu)) (composeC v (inverseC Hv)) a0).   rw H. tv. ufi composeC H0. rw H0. wr (prJ_recov a0). app R_inj.   wr ext_to_prod_prop. rw inverseC_prb. rw inverseC_prb. rw prJ_prop. tv.   rw H. rw inverseC_pra. wrr H. Qed. ```
Canonical decomposition of a function
``` Lemma canonical_decomposition1: forall f g i,   is_function f ->   g = restriction2 f (source f) (range (graph f)) ->   i = canonical_injection (range (graph f)) (target f) ->   (composable i g & f = compose i g & injective i & surjective g &   (injective f -> bijective g )). Proof. ir.   assert (Ha:sub (range (graph f)) (target f)). nin H. fprops.   assert (restriction2_axioms f (source f) (range (graph f))).   red. ee. am. app sub_refl. app Ha.   uf image_by_fun. app sub_image_by_graph.   assert (is_function g). rw H0. fprops.   assert (is_function i). rw H1. fprops.   assert (Hb: injective i). rw H1. app ci_injective.   assert (Hd:source f = source g). rw H0. uf restriction2. aw.   assert (Hc:surjective g). rw H0. app restriction2_surjective.   uf image_of_fun. red in H; ee. rw H6. rw image_by_graph_domain. tv.   fprops.   assert (composable i g). red. eee. rw H1. rw H0.   uf canonical_injection. uf restriction2. aw.   assert (f = compose i g). app function_exten. fct_tac.   rw H0. uf restriction2. aw. rw H1. uf canonical_injection. aw.   ir. aw.   rw H0. rw restriction2_W. rw H1. rw ci_W. tv. red in H; ee; red in H; ee; am.   rw range_inc_rw. exists x. au. am. am. am. ue.   eee. ir. red. ee. apply inj_right_compose with i. am. ue. am. Qed. ```
Restriction to its image
``` Definition imageC (a b:Set) (f:a->b) := IM (fun u:a => Ro (f u)). Lemma imageC_inc: forall (a b:Set) (f:a->b) (x:a), inc (Ro (f x)) (imageC f). Proof. ir. uf imageC. app IM_inc. exists x. tv. Qed. Lemma imageC_exists: forall (a b:Set) (f:a->b) x,   inc x (imageC f) -> exists y:a, x = Ro (f y). Proof. ir. ufi imageC H. cp (IM_exists H). nin H0. exists x0. sy. am. Qed. Lemma sub_image_targetC: forall (a b:Set) (f:a->b), sub (imageC f) b. Proof. ir. red. ir. cp (imageC_exists H). nin H0. rw H0. app R_inc. Qed. Definition restriction_to_image (a b:Set) (f:a->b) :=   fun x:a => Bo (imageC_inc f x). Lemma restriction_to_image_pr: forall (a b:Set) (f:a->b) (x:a),   Ro (restriction_to_image f x) = Ro (f x). Proof. ir. uf restriction_to_image. rw B_eq. tv. Qed. Lemma canonical_decomposition1C: forall (a b:Set) (f:a->b)   (g:a-> imageC f)(i:imageC f ->b),   g = restriction_to_image f ->   i = inclusionC (sub_image_targetC (f:=f)) ->   (injectiveC i & surjectiveC g &   (injectiveC f -> bijectiveC g )). Proof. ir. assert (surjectiveC g).   rw H. red. ir. assert (inc (Ro u) (imageC f)). app R_inc.   cp (imageC_exists H1). nin H2. exists x. app R_inj.   rw restriction_to_image_pr. sy; am. ir.   uf restriction_to_image.   ee. red. ir. assert (Ro (i u) = Ro (i v)). rww H2.   rwi H0 H3. rwi inclusionC_pr H3. rwi inclusionC_pr H3. app R_inj. am.   ir. red. ee. red. ir. assert (Ro (g u) = Ro (g v)). rw H3. tv.   rwi H H4. rwi restriction_to_image_pr H4. rwi restriction_to_image_pr H4.   app H2. app R_inj. am. Qed. End Bfunction. Export Bfunction. ```