Library set2
Require Export set1.
Set Implicit Arguments.
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.
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.
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.
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.
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.
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.
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.
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.
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.