- Fundamental set theory
- Theory of Sets EII-3 Correspondences
- EII-3-1 Graphs et correspondences
- Additional lemmas
- EII-3-2 Inverse of a correspondence
- EII-3-3 Composition of two correspondences
- EII-3-4 Functions
- EII-3-5 Restrictions and extensions of functions
- EII-3-6 Definition of a function by means of a term
- EII-3-7 Composition of two functions. Inverse function
- EII-3-8 Retractions and sections
- EII-3-9 Functions of two arguments
Library set3
Theory of Sets: EII-4 Union and intersection of a family of sets
Copyright INRIA (2009-2010) Apics Team (Jose Grimm).
Require Export set2.
Set Implicit Arguments.
Module Bunion.
Hint Resolve fcompose_fgraph nonempty_singleton: fprops.
Hint Resolve inc_V_range: fprops.
Bourbaki defines union and intersection of a functional graph
Record Uintegral (I :Set)(f :I->Set) : Set := {UI_z : I; UI_elt : f UI_z}.
Definition uniont (I:Set)(f : I->Set) :=
IM (fun i : Uintegral f => Ro (UI_elt i)).
Definition intersectiont (I:Set) (f : I->Set):=
Zo (uniont f) (fun y => forall z : I, inc y (f z)).
Definition unionf (x:Set)(f: Set->Set) := uniont (fun a:x => f (Ro a)).
Definition unionb (g:Set) := unionf (domain g)(fun a=> V a g).
Definition intersectionf (x:Set)(f: Set->Set):=
intersectiont(fun a:x => f (Ro a)).
Definition intersectionb (g:Set) := intersectionf (domain g) (fun a=> V a g).
Basic properties of union an intersection
Lemma uniont_rw: forall (I:Set) (f:I->Set) x,
inc x (uniont f) = exists z, inc x (f z).
Proof. ir. uf uniont. app iff_eq. ir. nin (IM_exists H).
exists (UI_z x0). wr H0. ap R_inc. ir. app IM_inc. nin H.
exists (Build_Uintegral f x0 (Bo H)). simpl. rww B_eq.
Qed.
Lemma unionf_rw: forall x i f,
inc x (unionf i f) = exists y, inc y i & inc x (f y).
Proof. ir. uf unionf. rw uniont_rw. app iff_eq. ir. nin H. exists (Ro x0).
ee. app R_inc. am. ir. nin H. ee. exists (Bo H). rw B_eq. am.
Qed.
Lemma unionb_rw: forall x f,
inc x (unionb f) = exists y, inc y (domain f) & inc x (V y f).
Proof. ir. uf unionb. rww unionf_rw.
Qed.
Hint Rewrite uniont_rw unionf_rw unionb_rw: sw.
Lemma uniont_inc : forall (I:Set) (f : I->Set) y x,
inc x (f y) -> inc x (uniont f).
Proof. ir. srw. exists y. am.
Qed.
Lemma uniont_exists : forall (I:Set) (f : I->Set) x,
inc x (uniont f) -> exists y:I, inc x (f y).
Proof. ir. srwi H. nin H. exists x0. am.
Qed.
Lemma unionf_inc: forall x y i f,
inc y i -> inc x (f y) -> inc x (unionf i f).
Proof. ir. srw. exists y. au.
Qed.
Lemma unionf_exists: forall x i f,
inc x (unionf i f) -> exists y, inc y i & inc x (f y).
Proof. ir. srwi H. am.
Qed.
Lemma unionb_inc: forall x y f,
inc y (domain f) -> inc x (V y f) ->
inc x (unionb f).
Proof. ir. srw. ex_tac.
Qed.
Lemma unionb_exists: forall x f,
inc x (unionb f) ->
exists y, inc y (domain f) & inc x (V y f).
Proof. ir. srwi H. am.
Qed.
Ltac union_tac:=
match goal with
| H:inc ?x (?f ?y) |- inc ?x (uniont ?f)
=> ap (uniont_inc f y H)
| Ha : inc ?i (domain ?g), Hb : inc ?x (V ?i ?g) |- inc ?x (unionb ?g)
=> ap (unionb_inc Ha Hb)
| Ha : inc ?x ?y, Hb : inc ?y ?a |- inc ?x (union ?a)
=> ap (union_inc Ha Hb)
| Ha : inc ?y ?i, Hb : inc ?x (?f ?y) |- inc ?x (unionf ?i ?f)
=> ap (unionf_inc _ Ha Hb)
| Ha : inc ?y ?i |- inc ?x (unionf ?i ?f)
=> apply unionf_inc with y; fprops
| Ha : inc ?i (domain ?g) |- inc ?x (unionb ?g)
=> apply unionb_inc with i; fprops
| Ha : inc ?y ?i |- inc ?x (unionf ?i ?f)
=> apply unionf_inc with y; fprops
| Ha : inc ?x (V ?i ?g) |- inc ?x (unionb ?g)
=> apply unionb_inc with i; fprops
| Hb : inc ?x (?f ?y) |- inc ?x (unionf ?i ?f)
=> apply unionf_inc with y; fprops
end.
Lemma intersectiont_rw: forall (I:Set) (f:I-> Set) x, nonemptyT I ->
inc x (intersectiont f) = (forall j, inc x (f j)).
Proof. ir. uf intersectiont. app iff_eq. ir. Ztac. app H2. ir. Ztac. srw.
nin H. exists H. app H0.
Qed.
Lemma intersectionf_rw : forall I f x, nonempty I ->
inc x (intersectionf I f) = (forall j, inc j I -> inc x (f j)).
Proof. ir. nin H. uf intersectionf. rw intersectiont_rw.
app iff_eq. ir. set (H0 (Bo H1)). rwi B_eq i. am. ir. app H0. app R_inc.
app (inc_nonempty H).
Qed.
Lemma intersectionb_rw : forall g x, nonempty g ->
inc x (intersectionb g) = (forall i, inc i (domain g) -> inc x (V i g)).
Proof. ir. uf intersectionb. rw intersectionf_rw. tv. nin H. uf domain.
exists (P y). aw. ex_tac.
Qed.
Hint Rewrite intersectiont_rw intersectionf_rw intersectionb_rw: sw.
Lemma intersectiont_inc : forall (I:Set) (f:I-> Set) x, nonemptyT I ->
(forall j, inc x (f j)) -> inc x (intersectiont f).
Proof. ir. srw.
Qed.
Lemma intersectiont_forall : forall (I:Set) (f:I-> Set) x j,
inc x (intersectiont f) -> inc x (f j).
Proof. ir. srwi H. app H. app nonemptyT_intro.
Qed.
Lemma intersectionf_inc :forall I f x, nonempty I ->
(forall j, inc j I -> inc x (f j)) -> inc x (intersectionf I f).
Proof. ir. srw.
Qed.
Lemma intersectionf_forall :forall I f x j,
inc x (intersectionf I f) -> inc j I -> inc x (f j).
Proof. ir. srwi H. app H. ex_tac.
Qed.
Lemma intersectionb_inc : forall g x, nonempty g ->
(forall i, inc i (domain g) -> inc x (V i g)) -> inc x (intersectionb g).
Proof. ir. srw.
Qed.
Lemma intersectionb_forall : forall g x i,
inc x (intersectionb g) -> inc i (domain g) -> inc x (V i g).
Proof. ir. srwi H. app H. ufi domain H0. awi H0.
nin H0. ee. ex_tac.
Qed.
Lemma intersectiont_empty: forall (I:Set) (f:I-> Set),
~ (nonemptyT I) -> (intersectiont f) = emptyset.
Proof. ir. empty_tac. ufi intersectiont H0. Ztac. srwi H1. nin H1. elim H.
app nonemptyT_intro.
Qed.
Lemma intersectionf_empty: forall f,
(intersectionf emptyset f) = emptyset.
Proof. ir. uf intersectionf. app intersectiont_empty. red. ir. nin H.
elim H.
Qed.
Lemma intersectionb_empty: forall f,
f = emptyset -> (intersectionb f) = emptyset.
Proof. ir. assert (domain f = emptyset). uf domain. empty_tac. awi H0.
nin H0. nin H0. rwi H H0. empty_tac. uf intersectionb. rw H0.
app intersectionf_empty.
Qed.
Lemma uniont_extensionality: forall (I:Set) (f: I-> Set) (f':I->Set),
(forall i, f i = f' i) -> uniont f = uniont f'.
Proof. ir. set_extens; srw ; srwi H0; nin H0; exists x0; [ wrr H | rww H].
Qed.
Lemma unionf_extensionality: forall sf f f',
(forall i, inc i sf -> f i = f' i) -> unionf sf f = unionf sf f'.
Proof. ir. set_extens; srw; srwi H0; nin H0; nin H0; ex_tac; [ wrr H | rww H].
Qed.
Lemma unionb_extensionality: forall f f',
f = f' -> unionb f = unionb f'.
Proof. ir. ue.
Qed.
Lemma intersectiont_extensionality:
forall (I:Set) (f:I-> Set) (f':I-> Set),
(forall i, f i = f' i) -> (intersectiont f) = (intersectiont f').
Proof. ir. nin (p_or_not_p (nonemptyT I)).
set_extens; srw; srwi H1. ir. wrr H. am. ir. rww H. am.
rww intersectiont_empty. rww intersectiont_empty.
Qed.
Lemma intersectionf_extensionality: forall I f f',
(forall i, inc i I -> f i = f' i) ->
intersectionf I f = intersectionf I f'.
Proof. ir. nin (emptyset_dichot I). rw H0.
rw intersectionf_empty. rww intersectionf_empty.
set_extens; srw; srwi H1. ir. wrr H. app H1. am. ir. rww H. app H1. am.
Qed.
Lemma intersectionb_extensionality: forall g g',
g = g' -> intersectionb g = intersectionb g'.
Proof. ir. ue.
Qed.
Lemma uniont_sub: forall (I:Set) (f: I-> Set) i,
sub (f i) (uniont f).
Proof. ir. red. ir. union_tac.
Qed.
Lemma intersectiont_sub: forall (I:Set) (f: I-> Set) i,
sub (intersectiont f) (f i).
Proof. ir. red. ir. srwi H. app H. app nonemptyT_intro.
Qed.
Lemma sub_uniont: forall (I:Set) (f: I-> Set) x,
(forall i, sub (f i) x) -> sub (uniont f) x.
Proof. ir. red. ir. srwi H0. nin H0. app (H x1).
Qed.
Lemma sub_intersectiont: forall (I:Set) (f: I-> Set) x,
nonemptyT I ->
(forall i, sub x (f i)) -> sub x (intersectiont f).
Proof. ir. red. ir. srw. ir. app H0.
Qed.
Lemma intersectiont_sub2: forall (I:Set) (f: I-> Set) x,
(forall i, sub (f i) x) -> sub (intersectiont f) x.
Proof. ir. nin (p_or_not_p (nonemptyT I)). red. ir. srwi H1.
nin H0. app (H H0). am. rww intersectiont_empty. app emptyset_sub_any.
Qed.
Lemma sub_uniont2: forall (I:Set) (f: I-> Set) x,
nonemptyT I -> (forall i, sub x (f i)) -> sub x (uniont f).
Proof. ir. red. ir. srw. nin H. exists H. app (H0 H).
Qed.
Lemma empty_uniont1: forall (I:Set) (f: I-> Set),
nonempty (uniont f) -> nonemptyT I.
Proof. ir. nin H. srwi H. nin H. app nonemptyT_intro.
Qed.
Lemma empty_unionf1: forall sf f,
nonempty (unionf sf f) -> nonempty sf.
Proof. ir. nin H. srwi H. nin H. ee. ex_tac.
Qed.
Lemma empty_unionf: forall sf f,
sf = emptyset -> unionf sf f = emptyset.
Proof. ir. empty_tac. srwi H0. nin H0. nin H0.
rwi H H0. elim (emptyset_pr H0).
Qed.
Proposition 1 : union (compose g f)
Theorem uniont_rewrite: forall (I K:Set) (f: K->I) (g:I ->Set),
surjectiveC f ->
uniont g = uniont (fun k:K => g(f k)).
Proof. ir. set_extens; srwi H0; srw; nin H0. nin (H x0).
exists x1. rww H1. exists (f x0). am.
Qed.
Theorem intersectiont_rewrite: forall (I K:Set) (f: K->I) (g:I ->Set),
surjectiveC f ->
intersectiont g = intersectiont (fun k:K => g(f k)).
Proof. ir. nin (p_or_not_p (nonemptyT K)). assert (nonemptyT I).
nin H0. set (f H0). app nonemptyT_intro.
set_extens; srwi H2;srw. ir. nin (H j). wr H3. app H2.
assert (~ nonemptyT I). dneg. nin H1. nin (H H1). app nonemptyT_intro.
do 2 rww intersectiont_empty.
Qed.
Lemma set_extens_aux: forall a b,
(forall x, (inc x a = inc x b)) -> a = b.
Proof. ir. set_extens. wrr H. rww H. Qed.
Lemma unionb_rewrite1: forall f g,
is_function f -> fgraph g -> range (graph f) = domain g ->
unionb g = unionb (fcompose g (graph f)).
Proof. ir. destruct H as [_ [ Ha _]].
assert (Hb: fcomposable g (graph f)). red. eee.
app set_extens_aux. ir. srw. rww (fcomposable_domain Hb). wr H1. app iff_eq.
ir. nin H. ee. srwi H. nin H. nin H. ex_tac. bw. ue. am.
ir. nin H. nin H. bwi H2. exists (V x0 (graph f)). rw H1. eee. am. am.
Qed.
Lemma unionb_rewrite: forall f g,
fgraph f -> range f = domain g ->
unionb g = unionb (gcompose g f).
Proof. ir. uf gcompose. set_extens; srwi H1;nin H1; ee. wri H0 H1.
srwi H1. nin H1. ee. srw. bw. exists x1. ee. am. bw. ue. am.
bwi H1. bwi H2. union_tac. wr H0. bwi H1. fprops. am.
Qed.
Lemma intersectionb_rewrite: forall f g,
fgraph f -> range f = domain g ->
intersectionb g = intersectionb (gcompose g f).
Proof. ir. nin (emptyset_dichot g).
assert (gcompose g f = emptyset). empty_tac. ufi gcompose H2.
ufi L H2. awi H2. nin H2. nin H2. awi H2. nin H2.
assert (inc x0 (range f)). aw. ex_tac. fprops. rwi H0 H4.
ufi domain H4. awi H4. nin H4. nin H4. rwi H1 H4. empty_tac. fprops.
rw H2. rww H1. assert (nonempty (gcompose g f)). uf gcompose.
nin H1. assert (inc (P y) (range f)). rw H0. uf domain. aw. ex_tac. awi H2.
nin H2. exists (J x (V (V x f) g)). uf L. aw. exists x. split. aw. ex_tac.
fprops. tv. fprops.
uf gcompose. set_extens; srwi H3;srw.
bw. ir. bw. app H3. wr H0. fprops.
ir. wri H0 H4. srwi H4. nin H4. ee. bwi H3.
cp (H3 _ H4). bwi H6. ue. am. am.
Qed.
Union and intersection of a function with singleton range
Lemma uniont_constant_alt: forall (I:Set) (f:I ->Set) (x:I),
is_constant_functionC f -> uniont f = f x.
Proof. ir. set_extens. nin(uniont_exists H0). rw (H x x1). am.
union_tac. Qed.
Lemma intersectiont_constant_alt: forall (I:Set) (f:I ->Set) (x:I),
is_constant_functionC f -> intersectiont f = f x.
Proof. ir. set_extens.
ap (intersectiont_forall (f:=f) x H0).
app intersectiont_inc. app nonemptyT_intro. ir. rw (H j x). am.
Qed.
Lemma singleton_type_inj: forall x (y:singleton x)(z:singleton x),
y = z.
Proof. ir. app R_inj. assert (inc (Ro y) (singleton x)). app R_inc.
assert (inc (Ro z) (singleton x)). app R_inc.
rw (singleton_eq H). db_tac.
Qed.
Lemma uniont_singleton:forall (a:Set) (x:a) (f: singleton (Ro x) -> Set),
uniont f = f (Bo (singleton_inc (Ro x))).
Proof. ir. set_extens. nin (uniont_exists H).
assert (x1 = (Bo (singleton_inc (Ro x)))). app singleton_type_inj.
wrr H1. union_tac.
Qed.
Lemma intersectiont_singleton:forall (a:Set)(x:a) (f: singleton (Ro x) -> Set),
intersectiont f = f (Bo (singleton_inc (Ro x))).
Proof. ir. set (j:= Bo (singleton_inc (Ro x))). set_extens.
app (intersectiont_forall (f:=f) j H). app intersectiont_inc.
app nonemptyT_intro. ir. assert (j = j0). app singleton_type_inj. wrr H0.
Qed.
Lemma unionf_singleton:forall f x,
unionf (singleton x) f = f x.
Proof. ir. set_extens. nin (unionf_exists H). ee.
wrr (singleton_eq H0).
assert (inc x (singleton x)). fprops. union_tac.
Qed.
Lemma intersectionf_singleton: forall f x,
intersectionf (singleton x) f = f x.
Proof. ir. assert (inc x (singleton x)). fprops.
set_extens. app (intersectionf_forall H0 H).
app intersectionf_inc. ex_tac. ir. db_tac.
Qed.
Lemma constant_function_pr: forall (a:Set) (h:a->Set) (x:a),
is_constant_functionC h ->
exists f: a->singleton (Ro x), exists g:singleton (Ro x)->Set,
(forall u:a, h u = g (f u)) & (g (Bo (singleton_inc (Ro x))) = h x).
Proof. ir. set (w:=Bo (singleton_inc (Ro x))). exists (fun u:a=> w).
exists (fun t:singleton (Ro x) => h x). ee. red in H. ir. app H. tv.
Qed.
Lemma uniont_constant: forall (I:Set) (f:I ->Set) (x:I),
is_constant_functionC f -> uniont f = f x.
Proof. ir. ap set_extens_aux; ir; srw. app iff_eq. ir. nin H0. rww (H x x1).
ir. exists x. am.
Qed.
Lemma intersectiont_constant: forall (I:Set) (f:I ->Set) (x:I),
is_constant_functionC f -> intersectiont f = f x.
Proof. ir. ap set_extens_aux; ir; srw. app iff_eq. ir. rww (H j x).
app nonemptyT_intro.
Qed.
Link between union and unionb
Lemma union_prop: forall x, union x = unionf x (fun u => u).
Proof. ir. set_extens. nin (union_exists H). nin H0.
app (unionf_inc (fun u=> u) H1 H0).
nin (unionf_exists H). nin H0. union_tac.
Qed.
Lemma intersection_prop: forall x, nonempty x ->
intersection x = intersectionf x (fun u => u).
Proof. ir. set_extens. app intersectionf_inc. ir.
ap (intersection_forall H0 H1).
app intersection_inc. ir. ap (intersectionf_forall H0 H1).
Qed.
Lemma unionb_alt: forall f, fgraph f -> unionb f = union (range f).
Proof. ir. rw union_prop. uf unionb.
set_extens. srwi H0. nin H0. ee. srw. exists (V x0 f). split. fprops. am.
srwi H0. nin H0. ee. srwi H0. nin H0. ee. union_tac. ue. am.
Qed.
Lemma unionb_identity: forall x, unionb (identity_g x) = union x.
Proof. ir. uf unionb. rw identity_domain. rw union_prop.
app unionf_extensionality. ir. rww identity_ev.
Qed.
Lemma union_singleton: forall x,
union (singleton x) = x.
Proof. ir. cp (unionf_singleton (fun u=> u) x). wrii union_prop H.
Qed.
Lemma intersection_singleton: forall x,
intersection (singleton x) = x.
Proof. ir. cp (intersectionf_singleton (fun u=> u) x).
wrii intersection_prop H. fprops.
Qed.
Monotony properties
Lemma union_monotone: forall (I:Set) (f g:I->Set),
(forall i, sub (f i) (g i)) -> sub (uniont f) (uniont g).
Proof. ir. red. ir. nin (uniont_exists H0). cp ((H x0) _ H1). union_tac.
Qed.
Lemma intersection_monotone: forall (I:Set) (f g:I->Set),
(forall i, sub (f i) (g i)) -> sub (intersectiont f) (intersectiont g).
Proof. ir. nin (p_or_not_p (nonemptyT I)).
intro x. srw. ir. app H. repeat rww intersectiont_empty. fprops.
Qed.
Lemma union_monotone2: forall A B f,
sub A B -> sub (unionf A f) (unionf B f).
Proof. ir. red. ir. nin (unionf_exists H0). ee.
cp (H _ H1). union_tac.
Qed.
Lemma intersection_monotone2: forall A B f,
sub A B -> nonempty A ->
sub (intersectionf B f) (intersectionf A f).
Proof. ir. assert (nonempty B). nin H0. exists y. app H.
intro x. srw. ir. app H2. app H.
Qed.
Associativity of union and intersection
Theorem union_assoc: forall sf sg f g,
sf = unionf sg g ->
unionf sf f = unionf sg (fun l => unionf (g l) f).
Proof. ir. rw H. set_extens; nin (unionf_exists H0); nin H1.
nin (unionf_exists H1). nin H3. union_tac. union_tac.
nin (unionf_exists H2). nin H3. union_tac. union_tac.
Qed.
Theorem intersection_assoc: forall sf sg f g,
(forall i, inc i sg -> nonempty (g i)) ->
sf = unionf sg g ->
intersectionf sf f = intersectionf sg (fun l => intersectionf (g l) f).
Proof. ir. rw H0. nin (emptyset_dichot sg). rw H1.
rww empty_unionf. rww intersectionf_empty. rww intersectionf_empty.
assert (nonempty (unionf sg g)). nin H1. nin (H _ H1). exists y0. union_tac.
app set_extens_aux; intro x. srw; app iff_eq; ir. srw. ir. app H3. union_tac.
app H. nin (unionf_exists H4). nin H5.
ap (intersectionf_forall (H3 _ H5) H6).
Qed.
Theorem image_of_union: forall (I:Set) (f:I->Set) g,
is_correspondence g ->
image_by_fun g (uniont f) =
uniont (fun i => image_by_fun g (f i)).
Proof. ir. assert (Ha: is_graph (graph g)). fprops. uf image_by_fun.
set_extens. awi H0. nin H0. ee. cp (uniont_exists H0).
nin H2. ee. apply uniont_inc with x1. aw. exists x0. intuition.
srwi H0. nin H0. ee. awi H0. nin H0. aw. exists x1. ee. union_tac. am.
Qed.
Theorem image_of_intersection: forall (I:Set) (f:I->Set) g,
is_correspondence g ->
sub (image_by_fun g (intersectiont f))
(intersectiont (fun i => image_by_fun g (f i))).
Proof. ir. uf image_by_fun. assert (is_graph (graph g)). fprops.
red. ir. awi H1. nin H1. ee. nin (p_or_not_p (nonemptyT I)).
app intersectiont_inc.
ir. aw. exists x0. ee. rwi intersectiont_rw H1. app H1. am. am.
rwi intersectiont_empty H1. empty_tac. am.
Qed.
Theorem inv_image_of_intersection: forall (I:Set) (f:I->Set) g,
is_function g ->
(inv_image_by_fun g (intersectiont f)) =
(intersectiont (fun i => inv_image_by_fun g (f i))).
Proof. ir.
assert (Ha: (is_graph (graph g))). fprops. app extensionality.
rw inv_image_by_fun_pr.
rww (intersectiont_extensionality (fun i => inv_image_by_fun g (f i))
(fun i => image_by_fun (inverse_fun g) (f i)) ).
app image_of_intersection. app inverse_correspondence. fct_tac. ir.
uf inv_image_by_fun. wrr inv_image_by_fun_pr. uf inv_image_by_fun.
red. ir. nin (p_or_not_p (nonemptyT I)). srwi H0. cp H1. nin H1.
cp (H0 H1). awi H3. nin H3. ee. aw. exists x0. split. srw.
ir. cp (H0 j). awi H5. nin H5. ee. wri (W_pr H H6) H5. wr (W_pr H H4). am. am.
am. rwi intersectiont_empty H0. empty_tac. am.
Qed.
Lemma inj_image_of_intersection: forall (I:Set) (f:I->Set) g,
injective g ->
(image_by_fun g (intersectiont f))
= (intersectiont (fun i => image_by_fun g (f i))).
Proof. ir. set(h := restriction2 g (source g) (range (graph g))).
set (i:= canonical_injection (range (graph g)) (target g)) .
assert (is_function g). fct_tac.
assert (Hw: intersection2 (graph g) (product (source g) (target g))=
graph g). nin H0. red in H0. wrr intersection2_sub. nin H0. red in H2.
am.
cp (canonical_decomposition1 H0 (refl_equal h) (refl_equal i)).
ee. cp (H5 H).
assert(forall a, image_by_fun g a = inv_image_by_fun (inverse_fun h) a).
uf inv_image_by_fun. uf inv_image_by_graph. uf inverse_fun. aw.
rw inverse_graph_involutive. uf h. uf restriction2. aw. rw Hw. tv.
uf h. uf restriction2. aw. rw Hw. fprops. rw H7.
rww (intersectiont_extensionality (fun i0 => image_by_fun g (f i0))
(fun i0 => inv_image_by_fun (inverse_fun h)(f i0))).
app inv_image_of_intersection. app bijective_inv_function.
Qed.
Theorem complementary_union: forall (I:Set) (f:I-> Set) x,
(forall i, sub (f i) x) -> nonemptyT I ->
complement x (uniont f) = intersectiont (fun i=> complement x (f i)).
Proof. ir. app set_extens_aux; intros u; srw; app iff_eq; ir. srw. eee.
dneg. exists j. tv.
nin H0. set (H1 H0). srwi i. eee. red. ir. nin H4.
set (H1 x0). srwi i. eee.
Qed.
Theorem complementary_intersection: forall (I:Set) (f:I-> Set) x,
(forall i, sub (f i) x) -> nonemptyT I ->
complement x (intersectiont f) = uniont (fun i=> complement x (f i)).
Proof. ir. set (g:= fun i => complement x (f i)).
assert (forall i, sub (g i) x). ir. uf g.
app sub_complement. cp (complementary_union g H1 H0).
assert (forall i, complement x (g i) = f i). uf g. ir.
srw. wr (intersectiont_extensionality _ f H3). wr H2. srw. app sub_uniont.
Qed.
Lemma union_of_twosets_aux: forall x y f,
unionf(doubleton x y) f = union2 (f x) (f y).
Proof. ir. set_extens. nin (unionf_exists H). ee.
nin (doubleton_or H0); wr H2; inter2tac.
nin (union2_or H). union_tac. union_tac.
Qed.
Lemma intersection_of_twosets_aux: forall x y f,
intersectionf(doubleton x y) f = intersection2 (f x) (f y).
Proof. ir. set_extens. inter2tac.
app (intersectionf_forall H (doubleton_first x y)).
app (intersectionf_forall H (doubleton_second x y)).
app intersectionf_inc. app nonempty_doubleton.
ir. nin (doubleton_or H0);rw H1;inter2tac.
Qed.
Lemma union_of_twosets: forall x y,
unionf(doubleton x y)(fun w => w) = union2 x y.
Proof. ir. rww union_of_twosets_aux.
Qed.
Lemma intersection_of_twosets: forall x y,
intersectionf(doubleton x y)(fun w => w) = intersection2 x y.
Proof. ir. rww intersection_of_twosets_aux.
Qed.
Lemma union_doubleton: forall x y,
union2 (singleton x)(singleton y) = doubleton x y.
Proof. ir. set_extens. nin (union2_or H); db_tac.
nin (doubleton_or H); rw H0; [app union2_first | app union2_second]; fprops.
Qed.
Lemma union2assoc: forall x y z,
union2 x (union2 y z) = union2 (union2 x y) z.
Proof. ir. set_extens; nin (union2_or H).
ap union2_first; app union2_first.
nin (union2_or H0). ap union2_first; app union2_second.
app union2_second.
nin (union2_or H0).
app union2_first. ap union2_second; app union2_first.
ap union2_second; app union2_second.
Qed.
Lemma intersection2assoc: forall x y z,
intersection2 x (intersection2 y z) = intersection2 (intersection2 x y) z.
Proof. ir. set_extens; nin (intersection2_both H);
[ nin (intersection2_both H1) | nin (intersection2_both H0) ] ;
inter2tac;inter2tac.
Qed.
Lemma intersection_union_distrib1: forall x y z,
union2 x (intersection2 y z) = intersection2 (union2 x y) (union2 x z).
Proof. ir. set_extens. nin (union2_or H). repeat inter2tac.
inter2tac. app union2_second.
inter2tac. app union2_second. inter2tac.
nin (intersection2_both H).
nin (union2_or H0). inter2tac.
nin (union2_or H1). inter2tac.
app union2_second. inter2tac.
Qed.
Lemma intersection_union_distrib2: forall x y z,
intersection2 x (union2 y z) = union2 (intersection2 x y) (intersection2 x z).
Proof. ir. set_extens. nin (intersection2_both H); nin (union2_or H1).
app union2_first. inter2tac.
app union2_second. inter2tac.
nin (union2_or H); nin (intersection2_both H0); inter2tac; inter2tac.
Qed.
Lemma union2_comp: forall x y z,
complement z (union2 x y) = intersection2 (complement z x)(complement z y).
Proof. ir. set_extens. srwi H. ee. app intersection2_inc; srw;split;tv.
red. ir. app H0. inter2tac.
red. ir. app H0. inter2tac.
srw. nin (intersection2_both H).
srwi H1. srwi H0. ee. am. red. ir. nin (union2_or H4); contradiction.
Qed.
Lemma intersection2_comp: forall x y z,
sub x z -> sub y z ->
complement z (intersection2 x y) = union2 (complement z x)(complement z y).
Proof. ir. set_extens. srwi H1. ee.
apply use_complement with z. am. red. ir. srwi H3. ee. app H2.
inter2tac. apply use_complement with z. am. red. ir. app H4.
inter2tac. apply use_complement with z. am. red. ir. app H4. inter2tac.
apply use_complement with z. nin (union2_or H1). srwi H2. ee. am.
srwi H2. ee. am. rw double_complement. red. ir. nin (union2_or H1).
srwi H3. ee. app H4. inter2tac.
srwi H3. ee. app H4. inter2tac.
red. ir. ap H. inter2tac.
Qed.
Lemma union2_complement: forall x z,
sub x z -> union2 x (complement z x) = z.
Proof. ir. set_extens. nin (union2_or H0). app H. srwi H1.
ee. am. nin (inc_or_not x0 (complement z x)). ir. inter2tac.
ir. app union2_first. apply use_complement with z. am. am.
Qed.
Lemma intersection2_complement: forall x z,
sub x z -> intersection2 x (complement z x) = emptyset.
Proof. ir. empty_tac. nin (intersection2_both H0).
srwi H2. ee. elim H3. am.
Qed.
Lemma image_of_union2: forall g x y,
is_correspondence g ->
image_by_fun g (union2 x y) = union2 (image_by_fun g x)(image_by_fun g y).
Proof. ir. wr union_of_twosets_aux. wr union_of_twosets. uf unionf.
rww image_of_union.
Qed.
Lemma nonemptyT_doubleton: forall x y, nonemptyT (doubleton x y).
Proof. ir. rww nonemptyT_not_empty0. app nonempty_doubleton.
Qed.
Lemma image_of_intersection2: forall g x y,
is_correspondence g ->
sub (image_by_fun g (intersection2 x y))
(intersection2 (image_by_fun g x) (image_by_fun g y)).
Proof. ir. wr intersection_of_twosets.
wr (intersection_of_twosets_aux x y (fun i => image_by_fun g i)).
uf intersectionf.
app (image_of_intersection (f:=(fun a : doubleton x y => Ro a))).
Qed.
Lemma inv_image_of_intersection2: forall g x y,
is_function g ->
inv_image_by_fun g (intersection2 x y) =
intersection2 (inv_image_by_fun g x)(inv_image_by_fun g y).
Proof. ir. wr intersection_of_twosets.
wr (intersection_of_twosets_aux x y (fun i => inv_image_by_fun g i)).
uf intersectionf.
app (inv_image_of_intersection (fun a : doubleton x y => Ro a)).
Qed.
Lemma inj_image_of_intersection2: forall g x y,
injective g ->
image_by_fun g (intersection2 x y)
= intersection2 (image_by_fun g x)(image_by_fun g y).
Proof. ir. wr intersection_of_twosets.
wr (intersection_of_twosets_aux x y (fun i => image_by_fun g i)).
uf intersectionf.
app (inj_image_of_intersection (fun a : doubleton x y => Ro a)).
Qed.
Lemma inv_image_of_comp: forall f x,
is_function f -> sub x (target f) ->
inv_image_by_fun f (complement (target f) x) =
complement (inv_image_by_fun f (target f))(inv_image_by_fun f x).
Proof. ir. assert (Ha: is_graph (graph f)). fprops.
uf inv_image_by_fun. set_extens. awi H1. nin H1. ee. srwi H1. ee. srw. ee.
aw. ex_tac.
red. ir. awi H4. nin H4. ee. red in H; ee. wri is_functional H6. nin H6.
cp (H8 _ _ _ H2 H5).
app H3. rww H9.
srwi H1. ee. awi H1. awi H2. nin H1. ee. aw. ex_tac.
srw. ee. am. red. ir. app H2. ex_tac.
Qed.
Lemma inj_image_of_comp: forall f x,
injective f -> sub x (source f) ->
image_by_fun f (complement (source f) x) =
complement (image_by_fun f (source f))(image_by_fun f x).
Proof. ir. assert (Ha:is_function f). red in H; ee; am.
assert (Hb: is_graph (graph f)). fprops. uf image_by_fun.
set_extens. awi H1. nin H1. ee. srwi H1. ee.
srw. ee. aw. ex_tac.
red. ir. awi H4. nin H4. ee.
cp (injective_pr H H2 H5). app H3. ue.
srwi H1. ee. aw. awi H1. nin H1. ee. ex_tac. srw. ee. am. red. ir.
app H2. aw. ex_tac.
Qed.
We define a covering for a map, a function, and a set of sets
Definition covering f x := fgraph f & sub x (unionb f).
Definition covering_f sf f x := sub x (unionf sf f).
Definition covering_s f x := sub x (union f).
Lemma covering_pr: forall f x,
fgraph f -> covering f x = covering_s (range f) x.
Proof. ir. uf covering; uf covering_s. rww unionb_alt.
ap iff_eq; intuition.
Qed.
Lemma covering_f_pr: forall sf f x,
covering_f sf f x = covering_s (range (L sf f)) x.
Proof. ir. uf covering_f; uf covering_s. wr unionb_alt. uf unionb. bw.
rww (unionf_extensionality (sf:=sf) f (fun a : Set => V a (L sf f))).
ir. bw. gprops.
Qed.
Two definitions, second one will be used in set5
Definition coarser_covering sf f sg g :=
forall j, inc j sg -> exists i, inc i sf & sub (g j) (f i).
Definition coarser_c y y':=
forall a, inc a y' -> exists b, inc b y & sub a b.
Lemma coarser_same: forall sf f sg g ,
coarser_covering sf f sg g = coarser_c (range (L sf f))(range (L sg g)).
Proof. ir. uf coarser_c. uf coarser_covering. ap iff_eq. ir.
bwi H0. nin H0. ee. nin (H _ H0). ee. wr H1.
assert (inc (f x0) (range (L sf f))). bw. ex_tac. ex_tac.
ir. assert (inc (g j) (range (L sg g))). bw. ex_tac.
nin (H _ H1). ee. bwi H2. nin H2. ee. wri H4 H3. ex_tac.
Qed.
Lemma sub_covering: forall Ia Ib f x,
covering_f Ia f x -> covering_f Ib f x -> sub Ib Ia ->
coarser_covering Ia f Ib f.
Proof. ir. red. ir. exists j. ee. app H1. fprops.
Qed.
Definition intersection_covering f g :=
fun z => intersection2 (f (P z)) (g (Q z)).
Definition intersection_covering2 x y:=
range(L (product x y)(intersection_covering (fun w => w) (fun w => w))).
Lemma intersection_covering2_pr: forall x y z,
inc z (intersection_covering2 x y) =
exists a, exists b, inc a x & inc b y & intersection2 a b = z.
Proof. ir. uf intersection_covering2. uf intersection_covering. ap iff_eq. ir.
bwi H. nin H. awi H. ee.
exists (P x0). exists (Q x0). intuition.
ir. nin H; nin H. ee. bw.
exists (J x0 x1). ee. fprops. aw.
Qed.
Lemma intersection_is_covering: forall sf f sg g x,
covering_f sf f x -> covering_f sg g x ->
covering_f (product sf sg) (intersection_covering f g) x.
Proof. ir. red. red. ir.
set (H _ H1). srwi i. nin i. set (H0 _ H1). srwi i. nin i. ee.
apw unionf_inc (J x1 x2). fprops.
uf intersection_covering. aw. inter2tac.
Qed.
Lemma intersection_covering_coarser1: forall sf f sg g x,
covering_f sf f x -> covering_f sg g x ->
coarser_covering sf f (product sf sg) (intersection_covering f g).
Proof. ir. red. ir. exists (P j). awi H1. ee. am.
uf intersection_covering. red. ir. inter2tac.
Qed.
Lemma intersection_covering_coarser2: forall sf f sg g x,
covering_f sf f x -> covering_f sg g x ->
coarser_covering sg g (product sf sg) (intersection_covering f g).
Proof. ir. red. ir. exists (Q j). awi H1. ee. am.
uf intersection_covering. red. ir. inter2tac.
Qed.
Lemma intersection_covering_coarser3: forall sf f sg g sh h x,
covering_f sf f x -> covering_f sg g x -> covering_f sh h x ->
coarser_covering sf f sh h ->
coarser_covering sg g sh h ->
coarser_covering (product sf sg) (intersection_covering f g) sh h.
Proof. ir. red. ir. nin (H2 _ H4). nin (H3 _ H4). ee.
exists (J x0 x1). ee. fprops.
uf intersection_covering. aw. red. ir. inter2tac. app H8. app H7.
Qed.
Next four lemmas are a rewrite of above; they say that
intersection_covering2 is the supremum of both args
Lemma product_is_covering2: forall u v x,
covering_s u x -> covering_s v x ->
covering_s (intersection_covering2 u v) x.
Proof. ir. red. red. ir.
nin (union_exists (H _ H1)). nin (union_exists (H0 _ H1)). ee.
apply union_inc with (intersection2 x1 x2). inter2tac.
rw intersection_covering2_pr. exists x1. exists x2. intuition.
Qed.
Lemma intersection_cov_coarser1: forall f g x,
covering_s f x -> covering_s g x ->
coarser_c f (intersection_covering2 f g).
Proof. ir. red. ir. rwi intersection_covering2_pr H1. nin H1. nin H1. ee.
ex_tac. wr H3. red. ir. inter2tac.
Qed.
Lemma intersection_cov_coarser2: forall f g x,
covering_s f x -> covering_s g x ->
coarser_c g (intersection_covering2 f g).
Proof. ir. red. ir. rwi intersection_covering2_pr H1. nin H1. nin H1. ee.
ex_tac. wr H3. red. ir. inter2tac.
Qed.
Lemma intersection_cov_coarser3: forall f g h x,
covering_s f x -> covering_s g x -> covering_s h x ->
coarser_c f h ->
coarser_c g h ->
coarser_c (intersection_covering2 f g) h.
Proof. ir. red. ir. red in H2; red in H3. cp (H2 _ H4). cp (H3 _ H4).
nin H5; nin H6. ee. exists (intersection2 x0 x1). ee.
rw intersection_covering2_pr. exists x0. exists x1. intuition.
red. ir. inter2tac. app H8. app H7.
Qed.
Lemma image_of_covering: forall sf f g,
surjective g -> covering_f sf f (source g)
-> covering_f sf (fun w => image_by_fun g (f w)) (target g).
Proof. ir. red in H0. red. red. ir. nin (surjective_pr H H1). ee.
nin (unionf_exists (H0 _ H2)). nin H4. union_tac.
uf image_by_fun. aw. ex_tac.
Qed.
Lemma inv_image_of_covering: forall sf f g,
is_function g -> covering_f sf f (target g)
-> covering_f sf (fun w => inv_image_by_fun g (f w)) (source g).
Proof. ir. red. red. ir. assert (inc (W x g) (target g)). fprops.
set (H0 _ H2). srwi i. nin i. ee.
union_tac. uf inv_image_by_fun. aw. ex_tac. graph_tac.
Qed.
Lemma product_of_covering: forall sf f sg g x y,
covering_f sf f x -> covering_f sg g y ->
covering_f (product sf sg) (fun z => product (f (P z)) (g (Q z)))
(product x y).
Proof. ir. red. red. ir. awi H1. ee.
set (H _ H2); set (H0 _ H3). srwi i; srwi i0. nin i; nin i0.
ee. apply unionf_inc with (J x1 x2). fprops. aw. eee.
Qed.
Lemma agrees_on_covering: forall sf f x g g',
covering_f sf f x -> is_function g -> is_function g' ->
source g = x -> source g' = x ->
(forall i, inc i sf -> agrees_on (intersection2 x (f i)) g g') ->
agrees_on x g g'.
Proof. ir. red. ee. rw H2. fprops. rw H3. fprops. ir.
nin (unionf_exists (H _ H5)). ee. destruct (H4 _ H6) as [ _ [ _ p]].
app p. inter2tac.
Qed.
Definition function_prop f s t:=
is_function f & source f = s & target f = t.
Definition function_prop_sub f s t:=
is_function f & source f = s & sub (target f) t.
Lemma extension_covering1: forall sf f t h,
(forall i, inc i sf -> function_prop (h i)(f i) t ) ->
(forall i j, inc i sf -> inc j sf ->
agrees_on (intersection2 (f i) (f j)) (h i) (h j)) ->
exists g, function_prop g (unionf sf f) t &
graph g = (unionf sf (fun i => (graph (h i)))) &
range(graph g) = (unionf sf (fun i => (range (graph (h i))))) &
(forall i, inc i sf -> agrees_on (f i) g (h i)).
Proof. ir.
set (g:= corresp (unionf sf f) t (unionf sf (fun i => (graph (h i))))).
assert (source g = unionf sf f). uf g. aw.
assert (target g = t). uf g. aw.
assert (graph g = (unionf sf (fun i => graph (h i)))). uf g. aw.
assert (is_graph (unionf sf (fun i => graph (h i)))).
red. ir. nin (unionf_exists H4). ee. nin (H _ H5).
cp (function_graph H7). app H9.
assert (is_function g). uf g. app is_function_pr. red. split. am.
ir. srwi H5. srwi H6. nin H5; nin H6. ee.
nin (H _ H5). nin (H _ H6). set (W_pr2 H10 H9). set (W_pr2 H12 H8).
app pair_extensionality.
assert (is_graph (graph (h x0))). fprops. app H14.
assert (is_graph (graph (h x1))). fprops. app H14. rw e. rw e0. wr H7.
cp (H0 _ _ H5 H6). red in H14. ee. app H16.
inter2tac. wr H11. graph_tac. wr H13. rw H7. graph_tac.
red. ir. awi H5. nin H5. srwi H5. nin H5. nin H5. cp (H _ H5). red in H7. ee.
wr H9. graph_tac. am. set_extens. aw. nin (unionf_exists H5). ee.
cp (H _ H6). red in H8. ee. aw. exists (W x (h x0)). union_tac.
graph_tac. rww H9. awi H5. nin H5. nin (unionf_exists H5). ee.
union_tac. cp (H _ H6). red in H8. ee. wr H9. graph_tac. am.
exists g. ee. red. eee. am. rw H3.
set_extens. awi H6. nin H6. nin (unionf_exists H6). ee.
union_tac. aw. ex_tac. nin (H _ H7). fprops. am.
nin (unionf_exists H6). ee. awi H8. nin H8. aw. exists x1.
union_tac. nin (H _ H7). fprops.
ir. red. ee. rw H1. red. ir. union_tac. nin (H _ H6).
ee. rw H8. fprops. ir. nin (H _ H6).
assert (inc (J a (W a (h i))) (graph g)). rw H3. union_tac.
graph_tac. ee. ue. app W_pr.
Qed.
Lemma extension_covering: forall sf f t h,
(forall i, inc i sf -> function_prop (h i) (f i) t) ->
(forall i j, inc i sf -> inc j sf ->
agrees_on (intersection2 (f i) (f j)) (h i) (h j)) ->
exists_unique (fun g => function_prop g (unionf sf f) t &
(forall i, inc i sf -> agrees_on (f i) g (h i))).
Proof. ir. red. split. nin (extension_covering1 _ _ H H0). exists x. eee.
uf function_prop. ir. ee. app function_exten. ue. ue. ir.
assert (covering_f sf f (unionf sf f)). red. fprops.
assert (forall i,
inc i sf -> agrees_on (intersection2 (unionf sf f) (f i)) x y).
ir. red. ee. wr H7. app intersection2sub_first.
wr H4. app (intersection2sub_first).
ir. set (intersection2_second H12). cp (H3 _ H11). cp (H6 _ H11).
red in H14; red in H13. ee. rw (H18 _ i0). ap (H16 _ i0).
nin (agrees_on_covering H10 H1 H2 H7 H4 H11). nin H13. app H14. ue.
Qed.
We have two definitions for a partition; in one case, we add the constraint
that elements are nonempty
Definition disjoint x y := intersection2 x y = emptyset.
Definition mutually_disjoint f :=
(forall i j, inc i (domain f) -> inc j (domain f) ->
i = j \/ (disjoint (V i f) (V j f))).
Definition partition_s y x:=
(union y = x) &
(forall a b, inc a y -> inc b y -> a = b \/ disjoint a b).
Definition partition y x:=
(union y = x) &
(forall a, inc a y -> nonempty a) &
(forall a b, inc a y -> inc b y -> a = b \/ disjoint a b).
Definition partition_fam f x:=
fgraph f & mutually_disjoint f & unionb f = x.
Lemma mutually_disjoint_prop: forall f,
(forall i j y, inc i (domain f) -> inc j (domain f) ->
inc y (V i f) -> inc y (V j f) -> i=j) ->
mutually_disjoint f.
Proof. ir. red. ir. nin (equal_or_not i j). left. am. right. red.
app is_emptyset. red. ir. nin (intersection2_both H3).
elim H2. app (H _ _ _ H0 H1 H4 H5).
Qed.
Lemma mutually_disjoint_prop2: forall x f,
(forall i j y, inc i x -> inc j x ->
inc y (f i) -> inc y (f j) -> i=j) ->
mutually_disjoint (L x f).
Proof. ir. app mutually_disjoint_prop. bw. ir. bwi H2. bwi H3.
app (H _ _ _ H0 H1 H2 H3). am. am.
Qed.
Lemma partitionset_pr: forall y x,
partition y x -> partition_s y x.
Proof. uf partition; uf partition_s. ir. int.
Qed.
Lemma partition_same: forall y x,
partition_s y x -> partition_fam (identity_g y) x.
Proof. ir. red in H; red. ee. app identity_fgraph. red. rw identity_domain. ir.
rw identity_ev. rw identity_ev. app H0. am. am. rw unionb_identity. am.
Qed.
Lemma partition_same2: forall y x,
partition_fam y x -> partition_s (range y) x.
Proof. ir. red in H; red. ee. wr H1. rww unionb_alt.
ir. rwi (frange_inc_rw a H) H2. rwi (frange_inc_rw b H) H3.
nin H2. nin H3. ee. rw H5. rw H4. induction (H0 _ _ H2 H3).
left; rww H6. au.
Qed.
Lemma partitions_is_covering: forall y x,
partition_s y x -> covering_s y x.
Proof. ir. red in H. ee. red. rw H. fprops.
Qed.
Lemma partition_fam_is_covering: forall y x,
partition_fam y x -> covering y x.
Proof. ir. red in H. ee. red. eee.
Qed.
Lemma partition_inc_exists: forall f x y,
partition_fam f x -> inc y x -> exists i, (inc i (domain f) & inc y (V i f)).
Proof. ir. red in H. ee. wri H2 H0. nin (unionb_exists H0). nin H3. ex_tac.
Qed.
Lemma partition_inc_unique: forall f x i j y,
partition_fam f x -> inc i (domain f) -> inc y (V i f) ->
inc j (domain f) -> inc y (V j f) -> i = j.
Proof. ir. red in H. ee. nin (H4 i j H0 H2). am. red in H.
assert (inc y (intersection2 (V i f) (V j f))). inter2tac.
rwi H6 H7. nin H7. elim x0.
Qed.
Lemma disjoint_pr: forall a b,
(forall u, inc u a -> inc u b -> False) -> disjoint a b.
Proof. ir. red. empty_tac. ir. nin (intersection2_both H0).
app (H _ H1 H2).
Qed.
Lemma disjoint_complement : forall x y,
disjoint y (complement x y).
Proof. ir. app disjoint_pr. ir. srwi H0. intuition.
Qed.
Lemma disjoint_symmetric : forall x y,
disjoint x y -> disjoint y x.
Proof. uf disjoint. ir. rw intersection2comm. am.
Qed.
Lemma coarser_transitive : forall y y' y'',
coarser_c y y' -> coarser_c y' y'' -> coarser_c y y''.
Proof. ir. red. ir. nin (H0 _ H1). ee. nin (H _ H2). ee. ex_tac.
ap (sub_trans H3 H5).
Qed.
Lemma coarser_reflexive : forall y, coarser_c y y.
Proof. ir. red. ir. ex_tac. fprops.
Qed.
Lemma coarser_antisymmetric : forall y y' x,
partition y x -> partition y' x ->
coarser_c y y' -> coarser_c y' y -> y = y'.
Proof. assert (forall y y' x, partition y x -> partition y' x ->
coarser_c y y' -> coarser_c y' y -> sub y y').
ir. red. ir. red in H1. red in H2. nin (H2 _ H3). ee.
nin (H1 _ H4). ee. red in H. ee. nin (H8 _ H3).
nin (H9 x0 x2). wri H11 H7. assert (x0 = x1). app extensionality.
rww H12. red in H11. empty_tac1 (y0). inter2tac.
app H7. app H5. am. am. ir. ap extensionality.
app (H _ _ _ H0 H1 H2 H3). app (H _ _ _ H1 H0 H3 H2).
Qed.
Definition variant a x y := (fun z:Set => Yo (z = a) x y).
Definition variantL a b x y := L (doubleton a b) (variant a x y).
Lemma variant_if_rw: forall a x y z,
z = a -> variant a x y z = x.
Proof. ir. uf variant. rww Y_if_rw. Qed.
Lemma variant_if_not_rw: forall a x y z,
z <> a -> variant a x y z = y.
Proof. ir. uf variant. rww Y_if_not_rw. Qed.
Lemma variant_V_a : forall a b x y,
V a (variantL a b x y) = x.
Proof. ir. uf variantL. bw. app variant_if_rw. fprops. Qed.
Lemma variant_V_b : forall a b x y,
b <> a -> V b (variantL a b x y) = y.
Proof. ir. uf variantL. bw. app variant_if_not_rw. fprops. Qed.
Lemma variant_fgraph : forall a b x y,
fgraph (variantL a b x y).
Proof. ir. uf variantL. gprops. Qed.
Lemma variant_domain : forall a b x y,
domain (variantL a b x y) = doubleton a b.
Proof. ir. uf variantL. bw. Qed.
Definition variantLc f g:= variantL TPa TPb f g.
Lemma variantLc_fgraph : forall x y,
fgraph (variantLc x y).
Proof. ir. uf variantLc. uf variantL. gprops.
Qed.
Hint Resolve variant_fgraph variantLc_fgraph: fprops.
Lemma variantLc_domain: forall f g,
domain (variantLc f g) = two_points.
Proof. ir. uf variantLc. uf variantL. bw. app two_points_pr2.
Qed.
Hint Rewrite variantLc_domain: bw.
Lemma variantLc_domain_nonempty: forall f g,
nonempty (domain (variantLc f g)).
Proof. ir. bw. exists TPa. fprops.
Qed.
Lemma variant_V_ca : forall x y,
V TPa (variantLc x y) = x.
Proof. ir. uf variantLc. uf variantL. bw. app variant_if_rw. fprops.
Qed.
Lemma variant_V_cb : forall x y,
V TPb (variantLc x y) = y.
Proof. ir. uf variantLc. uf variantL. bw. app variant_if_not_rw.
ap two_points_distinctb. fprops.
Qed.
Hint Rewrite variant_V_ca variant_V_cb: bw.
Definition partition_with_complement x j :=
variantLc j (complement x j).
Lemma is_partition_with_complement: forall x j,
sub j x -> partition_fam (partition_with_complement x j) x.
Proof. ir. uf partition_with_complement. red. ee. ap variantLc_fgraph.
red. bw. ir. rwi two_points_pr H0. rwi two_points_pr H1.
nin H0. rw H0. nin H1. rw H1. left. tv. rw H1.
right. bw. app disjoint_complement.
nin H1; rw H0; rw H1; [right | left ]. bw.
app disjoint_symmetric. app disjoint_complement. tv.
uf unionb. uf variantLc. rw variant_domain. rw union_of_twosets_aux.
bw. app union2_complement.
Qed.
Greatest and least partition for covering order
Definition largest_partition x := range(L x (fun z => singleton z)).
Definition smallest_partition x := (singleton x).
Lemma partition_smallest: forall x,
nonempty x -> partition(smallest_partition x) x.
Proof. ir. uf smallest_partition. red. ee. app union_singleton.
ir. db_tac.
ir. left. rw (singleton_eq H0). db_tac.
Qed.
Lemma largest_partition_pr: forall x z,
inc z (largest_partition x) = exists w, inc w x & singleton w = z.
Proof. ir. uf largest_partition. app iff_eq. ir. bwi H. am.
ir. bw.
Qed.
Lemma partition_largest: forall x, partition (largest_partition x) x.
Proof. ir. red. ee. set_extens. nin (union_exists H).
ee. rwi largest_partition_pr H1. nin H1. ee. wri H2 H0.
db_tac.
apply union_inc with (singleton x0). fprops.
rw largest_partition_pr. ex_tac.
ir. rwi largest_partition_pr H. nin H. ee. wr H0. app nonempty_singleton.
ir. rwi largest_partition_pr H. rwi largest_partition_pr H0. nin H; nin H0.
ee. wr H2; wr H1. nin (equal_or_not x0 x1). left. rww H3. right.
app disjoint_pr. ir. elim H3. wr (singleton_eq H4). db_tac.
Qed.
Definition injective_graph f:=
fgraph f &
(forall x y, inc x (domain f) -> inc y (domain f) ->
V x f = V y f -> x = y).
Lemma injective_partition: forall f x,
partition_fam f x -> (forall i, inc i (domain f) -> nonempty (V i f))
-> injective_graph f.
Proof. ir. red. red in H. ee. am. ir. nin (H1 _ _ H3 H4). am.
red in H6. rwi H5 H6. rwi intersection2idem H6.
nin (H0 _ H4). rwi H6 H7. empty_tac.
Qed.
Lemma partition_fam_partition: forall f x,
partition_fam f x -> (forall i, inc i (domain f) -> nonempty (V i f))
-> partition(range f) x.
Proof. ir. cp (partition_same2 H). red. red in H1. ee. am.
ir. red in H. ee. awi H3. nin H3. set (pr2_V H H3). awi e.
rw e. app H0. aw. ex_tac. fprops. fprops. am.
Qed.
Lemma inv_image_disjoint : forall g x y,
is_function g -> disjoint x y ->
disjoint (inv_image_by_fun g x)(inv_image_by_fun g y).
Proof. ir. red. wrr inv_image_of_intersection2. red in H0. rw H0.
empty_tac. ufi inv_image_by_fun H1. awi H1. nin H1.
ee. nin H1. elim x1.
Qed.
Theorem extension_partition: forall f x t h,
partition_fam f x ->
(forall i, inc i (domain f) -> function_prop (h i) (V i f) t) ->
exists_unique (fun g => function_prop g x t &
(forall i, inc i (domain f) -> agrees_on (V i f) g (h i))).
Proof. ir. set (sf:= (domain f)). set (ff:= fun i => V i f).
assert(forall i j, inc i (domain f) -> inc j (domain f) ->
agrees_on (intersection2 (ff i) (ff j)) (h i) (h j)).
ir. unfold ff. red in H. ee. cp (H3 _ _ H1 H2). red. nin H5. rw H5.
assert (intersection2 (V j f) (V j f) = (V j f)). app intersection2idem.
rw H6. ee. nin (H0 _ H2). ee. rw H8. fprops.
nin (H0 _ H2). ee. rw H8. fprops. ir. tv.
red in H5. rw H5. ir. ee. app emptyset_sub_any. app emptyset_sub_any.
ir. nin H6. elim x0.
set (extension_covering ff h H0 H1). red in H. ee.
assert (unionb f = unionf (domain f) ff). tv. wri H4 e.
rwi H3 e. am.
Qed.
Theorem extension_partition1: forall f x t h,
partition_fam f x ->
(forall i, inc i (domain f) -> function_prop_sub (h i) (V i f) t) ->
exists g, function_prop g x t &
(forall i, inc i (domain f) -> agrees_on (V i f) g (h i)).
Proof. ir. set(nh := fun i=> corresp (V i f) t (graph (h i))).
assert(forall i, inc i (domain f) -> function_prop (nh i) (V i f) t). ir.
cp (H0 _ H1). red in H2; ee. red. uf nh. aw. eee. red. ee.
red in H2. ee. red. aw. split. app is_triple_corr. red.
nin H2. red in H7.
apply sub_trans with (product (source (h i)) (target (h i))).
am. app product_monotone. ue. aw. fprops. rw corresp_graph. aw. sy; am.
nin (extension_partition nh H H1). clear H3. nin H2.
exists x0. ee. am. ir. cp (H3 _ H4). red in H5; ee. red. ee. am.
cp (H0 _ H4). red in H8. ee. ue. ir. rw (H7 _ H8).
app W_pr. nin (H1 _ H4). am. uf nh. aw. graph_tac.
nin (H0 _ H4). am. nin (H0 _ H4). ee. ue.
Qed.
Theorem disjoint_union_lemma : forall f,
fgraph f -> exists g, exists x,
fgraph g & x = unionb g &
(forall i, inc i (domain f) -> equipotent (V i f) (V i g))
& mutually_disjoint g.
Proof. ir. set (a:= unionb f). set (sf:= domain f).
set (h:= fun i:sf => BL(fun w => J w (Ro i))(V (Ro i) f)(product a sf)).
assert (forall i:sf, source (h i) = V (Ro i) f). ir. uf h. aw.
assert (forall i, target (h i) = product a sf). ir. uf h. aw.
assert (forall i:sf, transf_axioms (fun w => J w (Ro i)) (V (Ro i) f)
(product a sf)).
ir. red. ir. app product_pair_inc. uf a. apply unionb_inc with (Ro i).
app R_inc. am. app R_inc.
assert (forall i:sf, is_function (h i)). ir. uf h. app bl_function.
set (g := IM (fun i:sf => J (Ro i) (image_of_fun (h i)))).
assert (fgraph g). uf g. red. ee. red. ir. nin (IM_exists H4). wr H5.
fprops. ir. nin (IM_exists H4). nin (IM_exists H5).
wri H7 H6; wri H8 H6. awi H6. cp (R_inj H6). wr H7; wr H8; wr H9; tv.
exists g. exists (unionb g). eee.
ir. set (j:= Bo H5). assert (inc (J (Ro j) (image_of_fun (h j))) g).
set (t:= V i g). uf g. app IM_inc. exists j. tv. cp (pr2_V H4 H6). awi H7.
assert (Ro j = i). uf j. app B_eq. rwi H8 H7. wr H7. uf h.
assert (restriction2_axioms (h j) (V i f) (image_of_fun (h j))).
red. ir. ee. uf h. app bl_function. rw H0. ue.
app sub_image_target.
uf image_of_fun. uf image_by_fun.
assert (source (h j) = V i f). uf h. rw H8. aw. ue.
exists (restriction2 (h j) (V i f) (image_of_fun (h j))).
ee. red. ee. app restriction2_injective. uf h. ap bl_injective. app H2.
ir. inter2tac. app restriction2_surjective. uf h. aw. ue. uf restriction2.
aw. uf restriction2. aw. assert (Ht: is_graph g). fprops.
red. ir. awii H5. awii H6. nin H5. cp (pr2_V H4 H5). awi H7. wr H7.
nin H6. cp (pr2_V H4 H6). awi H8. wr H8. ufi g H5. nin (IM_exists H5).
cp (pr1_def H9). wr (pr2_def H9). clear H9.
ufi g H6. nin (IM_exists H6). cp (pr1_def H9). wr (pr2_def H9).
clear H9. nin (equal_or_not i j). left. am. right.
app disjoint_pr. ir. elim H9.
ufi image_of_fun H12. ufi image_of_fun H13.
awi H12; awi H13. nin H12; nin H13. ee.
ufi h H14. ufi h H15. rwi H10 H15. rwi H11 H14.
assert (is_function (BL(fun w => J w i) (V i f)(product a sf))).
wr H10. app bl_function. cp (W_pr H16 H15).
assert (is_function (BL(fun w => J w j) (V j f)(product a sf))).
wr H11. app bl_function. cp (W_pr H18 H14). rwi bl_W H17.
rwi bl_W H19. wri H17 H19. sy. inter2tac. wr H11. app H2.
cp (inc_pr1graph_source H18 H14). awi H20. am. wr H10. app H2.
cp (inc_pr1graph_source H16 H15). awi H20. am.
Qed.
Definition disjoint_union_fam f :=
(L (domain f)(fun i => product (V i f) (singleton i))).
Definition disjoint_union f :=
unionb (disjoint_union_fam f).
Lemma disjoint_union_disjoint:
forall f, fgraph f ->
mutually_disjoint(disjoint_union_fam f).
Proof. ir. red. uf disjoint_union_fam. bw. ir. nin (equal_or_not i j).
left. am. right. app disjoint_pr. ir. elim H2. bwi H3. bwi H4.
awi H3. awi H4. ee. ue. am. am.
Qed.
Lemma partion_union_disjoint: forall f, fgraph f ->
partition_fam (disjoint_union_fam f) (disjoint_union f).
Proof. ir. red. ee. uf disjoint_union_fam. gprops.
app disjoint_union_disjoint. tv.
Qed.
Theorem disjoint_union_pr: forall f,
fgraph f -> exists x,
source x = disjoint_union f &
target x = unionb f &
surjective x &
(mutually_disjoint f -> bijective x).
Proof. ir.
set (aux:= (L (domain f) (fun i => product (V i f) (singleton i)))).
cp (partion_union_disjoint H).
assert (domain aux = domain f). uf aux. bw.
set (h:= fun i => BL P (product (V i f) (singleton i)) (unionb f)).
assert (forall i, inc i (domain aux) ->
transf_axioms P (product (V i f) (singleton i)) (unionb f)).
red. ir. awi H3. ee. union_tac. ue.
assert (forall i, inc i (domain aux) ->
function_prop (h i) (V i aux)(unionb f)). ir. uf h. red. ee.
app bl_function. app H2. uf aux. bw. aw. ue. aw.
nin (extension_partition _ H0 H3). clear H5.
nin H4. ee. red in H4; ee. assert (surjective x).
app surjective_pr5. ir. rwi H7 H8.
nin (unionb_exists H8). rw H6. ee. exists (J y x0). ee.
uf disjoint_union. apply unionb_inc with x0. uf disjoint_union_fam. bw.
uf disjoint_union_fam. bw. fprops.
assert (y = W (J y x0) x). wri H1 H9. cp (H5 _ H9). red in H11. ee.
ufi disjoint_union_fam H13. bwi H13.
assert (inc (J y x0) (product (V x0 f) (singleton x0))). fprops.
cp (H13 _ H14). ufi h H15. rwi bl_W H15. ue. aw. red. ir.
awi H16. ee. union_tac. ue. fprops.
wrr H1. red.
set (z:= J y x0). fold z in H11. rw H11. graph_tac. ue.
uf disjoint_union. apply unionb_inc with x0. uf disjoint_union_fam. bw.
uf disjoint_union_fam. bw. uf z. fprops.
exists x. eee. ir. red. ee. red. ee. am. rw H6. ir.
ufi disjoint_union H10; ufi disjoint_union H11.
cp (unionb_exists H10). clear H10. ufi disjoint_union_fam H13. bwi H13.
nin H13. ee. bwi H13. red in H9.
cp (unionb_exists H11). clear H11. ufi disjoint_union_fam H14. bwi H14.
nin H14. ee. bwi H14. cp (H9 _ _ H10 H11). clear H9.
assert (Ht: (domain (disjoint_union_fam f)) = domain f). wrr H1. rwi Ht H5.
cp (H5 _ H10); cp (H5 _ H11).
red in H9; red in H16. ee. ufi disjoint_union_fam H20. bwi H20. rwi H20 H12.
ufi disjoint_union_fam H18. bwi H18. rwi H18 H12.
ufi h H12. rwii bl_W H12. rwii bl_W H12.
awi H13; awi H14; ee. app pair_extensionality.
wri H24 H15; wri H22 H15. nin H15. am. red in H15.
empty_tac1 (P y). inter2tac. wrr H12. ue. ue.
app H2. ue. app H2. ue. am. am. am. am. am. am. am.
Qed.
Bourbaki has an axiom (not needed here) that says that the powerset exists
Lemma powerset_monotone: forall a b,
sub a b -> sub (powerset a) (powerset b).
Proof. ir. red. ir. ap powerset_inc. apply sub_trans with a.
app powerset_sub. am.
Qed.
Lemma powerset_emptyset :
powerset emptyset = singleton emptyset.
Proof. app set_extens_aux. ir. aw. ap sub_emptyset.
Qed.
Canonical extension of
f:E->F to powerset E -> powerset F
Definition extension_to_parts f :=
BL(image_by_fun f) (powerset (source f)) (powerset (target f)).
Lemma etp_axioms: forall f,
is_correspondence f ->
transf_axioms (image_by_fun f) (powerset (source f))
(powerset (target f)).
Proof. ir. red. ir. awi H0. aw.
uf image_by_fun. apw sub_trans (range (graph f)).
app sub_image_by_graph. fprops.
Qed.
Lemma etp_function: forall f,
is_correspondence f -> is_function (extension_to_parts f).
Proof. ir. uf extension_to_parts. app bl_function. app etp_axioms.
Qed.
Lemma etp_W: forall f x,
is_correspondence f -> sub x (source f)
-> W x (extension_to_parts f) = image_by_fun f x.
Proof. ir. uf extension_to_parts. aw. app etp_axioms.
Qed.
Hint Resolve etp_function : fprops.
Morphism properties of extension
Lemma etp_composable: forall f g,
composableC g f ->
composable (extension_to_parts g) (extension_to_parts f).
Proof. ir. red in H. ee. red. ee; fprops.
uf extension_to_parts. aw. ue.
Qed.
Lemma etp_compose: forall f g,
composableC g f ->
compose (extension_to_parts g) (extension_to_parts f)
= extension_to_parts (compose g f).
Proof. ir. assert (H1:=etp_composable H). red in H. ee.
assert (is_correspondence (compose g f)). app compose_correspondence.
ap function_exten. fct_tac.
fprops. uf extension_to_parts. aw. uf extension_to_parts. aw.
ir. ufi extension_to_parts H4. awi H4. aw.
repeat rww etp_W. sy. app compose_of_sets. aw.
rw H2. uf image_by_fun. apw sub_trans (range (graph f)).
app sub_image_by_graph. fprops. uf extension_to_parts. aw.
Qed.
Lemma etp_identity: forall x,
extension_to_parts (identity x) = identity (powerset x).
Proof. ir. set (@identity_corresp x).
ap function_exten. fprops. fprops.
uf extension_to_parts. aw. uf extension_to_parts. aw. ir.
ufi extension_to_parts H. awi H.
rww etp_W. srw.
set_extens. awi H0. nin H0. nin H0. srwi H1. ue. app H.
fprops. aw. aw. ex_tac. srw. app H.
fprops. aw. aw.
Qed.
Lemma composable_for_function: forall f g,
composable g f -> composableC g f.
Proof. ir. red in H. ee. red in H; red in H0. ee. red. au.
Qed.
Theorem etp_surjective: forall f,
surjective f -> surjective (extension_to_parts f).
Proof. ir. app surj_if_exists_right_inv.
nin (exists_right_inv_from_surj H). red in H0. ee.
exists (extension_to_parts x). red. split. app etp_composable.
app composable_for_function.
rw etp_compose. rw H1.
rw etp_identity. uf extension_to_parts. aw. app composable_for_function.
Qed.
Theorem etp_injective: forall f,
injective f -> injective (extension_to_parts f).
Proof. ir. nin (emptyset_dichot (source f)).
red. ee. fprops. red in H; ee; red in H; eee.
uf extension_to_parts. aw. rw H0. rw powerset_emptyset. ir.
rw (singleton_eq H1); db_tac.
nin (exists_left_inv_from_inj H H0). red in H1. ee.
app inj_if_exists_left_inv.
exists (extension_to_parts x). red. split.
app etp_composable. app composable_for_function. rw etp_compose.
rw H2. rw etp_identity. uf extension_to_parts. aw.
app composable_for_function.
Qed.
The set of functional graphs is denoted by F^E, the set of functions by calF(E; F)
Definition set_of_gfunctions x y:=
Zo (powerset (product x y))(fun z => fgraph z & x = domain z).
Definition set_of_functions x y :=
Zo (set_of_correspondences x y)
(fun z => fgraph (graph z) & x = domain (graph z)).
Definition set_of_permutations E :=
(Zo (set_of_functions E E)(fun z=> bijective z)).
Lemma set_of_functions_rw: forall x y f,
inc f (set_of_functions x y) =
(is_function f & source f = x & target f = y).
Proof. ir. uf is_function. uf set_of_functions. ap iff_eq. ir. Ztac.
rwi set_of_correspondences_rw H0. eee. ir. ee. Ztac.
rw set_of_correspondences_rw. eee. eee.
Qed.
Hint Rewrite set_of_functions_rw : aw.
Lemma inc_set_of_gfunctions: forall f,
is_function f -> inc (graph f) (set_of_gfunctions (source f) (target f)).
Proof. ir. uf set_of_gfunctions. nin H. nin H. Ztac. wrr corr_propa.
Qed.
Lemma set_of_gfunctions_inc: forall x y z,
inc z (set_of_gfunctions x y) -> exists f,
is_function f & source f = x & target f = y & graph f =z.
Proof. ir. ufi set_of_gfunctions H. Ztac. exists (corresp x y z). eee.
app is_function_pr. wri corr_propa H0. rwi corr_propc H0. ee. am.
aw. aw. aw.
Qed.
Definition set_of_sub_functions (x y: Set) :=
unionf(powerset x)(fun z=> (set_of_functions z y)).
Lemma set_of_sub_functions_rw: forall x y f,
inc f (set_of_sub_functions x y) =
(is_function f & sub (source f) x & target f = y).
Proof. ir. uf set_of_sub_functions. app iff_eq. ir. Ztac.
nin (unionf_exists H). nin H0. awi H1. eee. awi H0. am.
ir. nin H. apw unionf_inc (source f). ee. aw. aw. eee.
Qed.
Lemma empty_source_graph: forall f,
is_function f -> source f = emptyset -> graph f = emptyset.
Proof. ir. empty_tac. elim (emptyset_pr (x:=(P y))).
wr H0. graph_tac.
Qed.
Lemma empty_target_graph: forall f,
is_function f -> target f = emptyset -> graph f = emptyset.
Proof. ir. empty_tac.
assert (inc (P y) (source f)). graph_tac.
elim (emptyset_pr (x:=(W (P y) f))). ue.
Qed.
Lemma set_of_functions_extens: forall x y a b,
inc a (set_of_functions x y) -> inc b (set_of_functions x y) ->
graph a = graph b -> a = b.
Proof. ir. awi H. awi H0. ee. app function_exten1. ue.
Qed.
Lemma small_set_of_functions_source: forall y,
small_set (set_of_functions emptyset y).
Proof. ir. red. ir. app (set_of_functions_extens H H0).
awi H. awi H0. ee. do 2 rww empty_source_graph.
Qed.
Lemma small_set_of_functions_target: forall x ,
small_set (set_of_functions x emptyset).
Proof. red. ir. app (set_of_functions_extens H H0).
awi H. awi H0. ee. do 2 rww empty_target_graph.
Qed.
Lemma empty_set_of_functions_target: forall x y,
(x = emptyset \/ nonempty y) -> nonempty (set_of_functions x y).
Proof. ir. nin H. exists (BL (fun z:Set => z) x y). aw. eee.
app bl_function. red. ir. rwi H H0. elim (emptyset_pr H0).
nin H. exists (constant_function x y y0 H).
uf constant_function. aw. eee.
Qed.
Canonical isomorpphism between calF(E,F) and F^E
Lemma graph_axioms: forall x y,
transf_axioms graph (set_of_functions x y) (set_of_gfunctions x y).
Proof. ir. red. ir. awi H. ee. wr H0. wr H1. app inc_set_of_gfunctions.
Qed.
Lemma graph_bijective: forall x y,
bijective (BL graph (set_of_functions x y) (set_of_gfunctions x y)).
Proof. ir. app bl_bijective. app graph_axioms.
ir. app (set_of_functions_extens H H0 H1).
ir. nin (set_of_gfunctions_inc H). exists x0. aw. eee.
Qed.
Lemma set_of_functions_equipotent: forall x y,
equipotent (set_of_functions x y) (set_of_gfunctions x y).
Proof. ir. exists (BL graph (set_of_functions x y) (set_of_gfunctions x y)).
eee. app graph_bijective. aw. aw.
Qed.
Isomorphimn between calF(E,F) and calF(E',F') for equipotent sets
Definition compose3function u v :=
BL (fun f => compose (compose v f) u)
(set_of_functions (target u) (source v))
(set_of_functions (source u) (target v)).
Lemma c3f_axioms: forall u v,
is_function u -> is_function v ->
transf_axioms (fun f => compose (compose v f) u)
(set_of_functions (target u) (source v))
(set_of_functions (source u) (target v)).
Proof. ir. red. ir. awi H1. aw. ee; aw. fct_tac. fct_tac. sy; am. aw.
Qed.
Lemma c3f_function: forall u v,
is_function u -> is_function v -> is_function(compose3function u v).
Proof. ir. uf compose3function. app bl_function. app c3f_axioms.
Qed.
Lemma c3f_W: forall u v f,
is_function u -> is_function v ->
is_function f -> source f = target u -> target f = source v ->
W f (compose3function u v) = compose (compose v f) u.
Proof. ir. uf compose3function. aw. red. ir. app c3f_axioms. aw. eee.
Qed.
Theorem c3f_injective: forall u v,
surjective u -> injective v -> injective (compose3function u v).
Proof. ir. assert (is_function u). fct_tac.
assert (is_function v). fct_tac. uf compose3function. app bl_injective.
app c3f_axioms. ir.
nin (emptyset_dichot (source v)).
app (small_set_of_functions_target (x:= target u)). ue. ue.
nin (exists_right_inv_from_surj H).
nin (exists_left_inv_from_inj H0 H6). awi H3. awi H4. ee.
assert (Ha: composable v u0). red; int.
assert (Hb: composable v v0). red; int. nin H7.
assert (Hc: is_function (compose v u0)). fct_tac.
assert (Hd: is_function (compose v v0)). fct_tac.
set (f_equal (fun i => compose i x) H5). simpl in e.
rwii compose_assoc e. rwii (@compose_assoc (compose v v0) u x) e.
rwi H13 e. assert (source (compose v u0) = target u). aw.
wri H14 e. rwii compose_id_right e.
assert (source (compose v v0) = target u). aw. rwi H14 e. wri H15 e.
rwii compose_id_right e.
set (f_equal (fun i => compose x0 i) e). simpl in e0.
nin H8. ee. do 2 wri compose_assoc e0; tv. rwi H16 e0.
wri H12 e0. rwi (compose_id_left H3) e0.
rwi H12 e0. wri H10 e0. rwii compose_id_left e0. red; eee. aw. red; eee; aw.
Qed.
Theorem c3f_surjective: forall u v,
(nonempty (source u) \/ (nonempty (source v)) \/ (nonempty (target v))
\/ target u = emptyset) ->
injective u -> surjective v -> surjective (compose3function u v).
Proof. ir. assert (is_function u). fct_tac.
assert (is_function v). fct_tac. set (c3f_function H2 H3).
app surjective_pr6. ir.
assert (Ha: target (compose3function u v) =
(set_of_functions (source u) (target v))). uf compose3function. aw.
nin (emptyset_dichot (source u)).
assert (nonempty (set_of_functions (target u) (source v))).
assert (target u = emptyset \/ nonempty (source v)). nin H. nin H.
rwi H5 H. elim (emptyset_pr H). nin H. au. nin H. right. nin H.
nin (surjective_pr H1 H). ee. ex_tac. au.
app (empty_set_of_functions_target). nin H6. rwi H5 Ha.
assert (inc y0 (source (compose3function u v))). uf compose3function.
rww bl_source. ex_tac. app (small_set_of_functions_source (y:=target v)).
wr Ha. fprops. wrr Ha.
nin (exists_right_inv_from_surj H1). nin (exists_left_inv_from_inj H0 H5).
cp (source_right_inverse H6). cp (target_left_inverse H7).
red in H6; red in H7; ee. ir.
assert (Hb: is_function x). fct_tac.
assert (Hc: is_function x0). fct_tac. rwi Ha H4. awi H4. ee.
set (f:= (compose (compose x y) x0)). assert (is_function f). uf f.
fct_tac. fct_tac. ue. rww H9. aw.
assert (source f=target u). uf f. aw. nin H7;ee. am.
assert (target f= source v). uf f. aw. nin H6;ee. sy;am.
exists f. split. uf compose3function. aw. eee. rww c3f_W.
uf f. assert (composable x y). red. ee. am. am. ue.
assert (composable y x0). red; eee.
rww (@compose_assoc x y x0).
wrr (@compose_assoc v x (compose y x0)). rw H11.
assert (target(compose y x0) = target v). aw. wr H19. rw compose_id_left.
rww compose_assoc. rw H10. wr H12. rww compose_id_right. fct_tac.
red. eee. fct_tac. aw. sy; am.
Qed.
Lemma c3f_bijective: forall u v,
bijective u -> bijective v -> bijective (compose3function u v).
Proof. ir. nin H; nin H0. red. ir. ee.
app c3f_injective. app c3f_surjective.
nin (emptyset_dichot (target u)). auto.
nin H3. left. nin (surjective_pr H1 H3). ee. ex_tac.
Qed.
Isomorphism between calF(BxC,A) and calF(C, calF(B,A)) and calF(B, calF(C,A))
Definition partial_fun_axioms f :=
is_function f & exists a, exists b, source f = product a b.
Lemma partial_fun_axioms_pr : forall f,
partial_fun_axioms f ->
source f = product (domain (source f))(range (source f)).
Proof. ir. red in H. ee. nin H0; nin H0.
nin (emptyset_dichot x0). rwi H1 H0. srwi H0. rw H0. aw. srw. tv.
assert (domain (source f) = x). rw H0. app product_domain. rw H2.
nin (emptyset_dichot x). rwi H3 H0. srwi H0. rw H0. aw. srw. tv.
assert (range (source f) = x0). rw H0. app product_range. ue.
Qed.
Definition first_partial_fun f y:=
BL(fun x => W (J x y) f) (domain (source f)) (target f).
Definition second_partial_fun f x:=
BL(fun y => W (J x y) f) (range (source f)) (target f).
Definition first_partial_function f:=
BL(fun y => first_partial_fun f y) (range (source f))
(set_of_functions (domain (source f)) (target f)).
Definition second_partial_function f:=
BL(fun x => second_partial_fun f x) (domain (source f))
(set_of_functions (range (source f)) (target f)).
Definition first_partial_map b c a:=
BL (fun f=> first_partial_function f)
(set_of_functions (product b c) a)
(set_of_functions c (set_of_functions b a)).
Definition second_partial_map b c a:=
BL (fun f=> second_partial_function f)
(set_of_functions (product b c) a)
(set_of_functions b (set_of_functions c a)).
Lemma fpf_axioms: forall f y,
partial_fun_axioms f -> inc y (range (source f)) ->
transf_axioms (fun x => W (J x y) f) (domain (source f)) (target f).
Proof. ir. cp (partial_fun_axioms_pr H). red in H. ee. red. ir.
app inc_W_target. ue.
Qed.
Lemma spf_axioms: forall f x,
partial_fun_axioms f -> inc x (domain (source f)) ->
transf_axioms (fun y => W (J x y) f) (range (source f)) (target f).
Proof. ir. cp (partial_fun_axioms_pr H). red in H. ee. red. ir.
assert (inc (J x c) (source f)). ue. fprops.
Qed.
Lemma fpf_function :forall f y,
partial_fun_axioms f -> inc y (range (source f)) ->
is_function (first_partial_fun f y).
Proof. ir. uf first_partial_fun. app bl_function. app fpf_axioms.
Qed.
Lemma spf_function :forall f x,
partial_fun_axioms f -> inc x (domain (source f)) ->
is_function (second_partial_fun f x).
Proof. ir. uf second_partial_fun. app bl_function. app spf_axioms.
Qed.
Lemma fpf_W :forall f x y,
partial_fun_axioms f -> inc x (domain (source f)) ->
inc y (range (source f)) ->
W x (first_partial_fun f y) = W (J x y) f.
Proof. ir. uf first_partial_fun. rww bl_W. app fpf_axioms.
Qed.
Lemma spf_W :forall f x y,
partial_fun_axioms f -> inc x (domain (source f)) ->
inc y (range (source f)) ->
W y (second_partial_fun f x) = W (J x y) f.
Proof. ir. uf second_partial_fun. rww bl_W. app spf_axioms.
Qed.
Lemma fpfa_axioms: forall f,
partial_fun_axioms f ->
transf_axioms (fun y => (first_partial_fun f y))(range (source f))
(set_of_functions (domain (source f)) (target f)).
Proof. ir. red. ir. aw. ee; try app fpf_function; uf first_partial_fun; aw.
Qed.
Lemma spfa_axioms: forall f ,
partial_fun_axioms f ->
transf_axioms (fun x => second_partial_fun f x) (domain (source f))
(set_of_functions (range (source f)) (target f)).
Proof. ir. red. ir. aw. ee; try app spf_function; uf second_partial_fun; aw.
Qed.
Lemma fpfa_function: forall f,
partial_fun_axioms f -> is_function (first_partial_function f).
Proof. ir. uf first_partial_function. app bl_function. app fpfa_axioms.
Qed.
Lemma spfa_function: forall f ,
partial_fun_axioms f -> is_function (second_partial_function f).
Proof. ir. uf second_partial_function. app bl_function. app spfa_axioms.
Qed.
Lemma fpfa_W: forall f y,
partial_fun_axioms f -> inc y (range (source f)) ->
W y (first_partial_function f) = first_partial_fun f y.
Proof. ir. uf first_partial_function. rww bl_W. app fpfa_axioms.
Qed.
Lemma spfa_W: forall f x,
partial_fun_axioms f -> inc x (domain (source f)) ->
W x (second_partial_function f) = second_partial_fun f x.
Proof. ir. uf second_partial_function. rww bl_W. app spfa_axioms.
Qed.
Lemma fpfb_axioms: forall a b c,
nonempty b -> nonempty c ->
transf_axioms (fun f=> first_partial_function f)
(set_of_functions (product b c) a)
(set_of_functions c (set_of_functions b a)).
Proof. ir. red. ir. awi H1. ee. aw. split. app fpfa_function. red. ee. am.
exists b. exists c. tv. uf first_partial_function. aw. rw H2.
rww product_range. rw product_domain. rww H3. au. am.
Qed.
Lemma spfb_axioms: forall a b c,
nonempty b -> nonempty c ->
transf_axioms (fun f=> second_partial_function f)
(set_of_functions (product b c) a)
(set_of_functions b (set_of_functions c a)).
Proof. ir. red. ir. awi H1. ee. aw. split. app spfa_function. red. ee. am.
exists b. exists c. tv. uf second_partial_function. aw. rw H2. rw H3.
rww product_domain. rww product_range. au.
Qed.
Lemma fpfb_function: forall a b c,
nonempty a -> nonempty b -> is_function (first_partial_map a b c).
Proof. ir. uf first_partial_map. app bl_function. app fpfb_axioms.
Qed.
Lemma spfb_function: forall a b c,
nonempty a -> nonempty b -> is_function (second_partial_map a b c).
Proof. ir. uf second_partial_map. app bl_function. app spfb_axioms.
Qed.
Lemma fpfb_W: forall a b c f,
nonempty a -> nonempty b -> inc f (set_of_functions (product a b) c) ->
W f (first_partial_map a b c) = first_partial_function f.
Proof. ir. uf first_partial_map. aw. app fpfb_axioms.
Qed.
Lemma spfb_W: forall a b c f,
nonempty a -> nonempty b -> inc f (set_of_functions (product a b) c) ->
W f (second_partial_map a b c) = second_partial_function f.
Proof. ir. uf second_partial_map. aw. app spfb_axioms.
Qed.
Lemma fpfb_WW: forall a b c f x,
nonempty a -> nonempty b -> inc f (set_of_functions (product a b) c) ->
inc x (product a b) ->
W (P x) (W (Q x) (W f (first_partial_map a b c))) = W x f.
Proof. ir. rww fpfb_W. awi H1. ee.
assert (partial_fun_axioms f). red. ee. am. exists a. exists b. tv.
awi H2. ee. assert (inc (Q x) (range (source f))). rw H3. rww product_range.
rww fpfa_W. rww fpf_W. aw. rw H3. rww product_domain.
Qed.
Lemma spfb_WW: forall a b c f x,
nonempty a -> nonempty b -> inc f (set_of_functions (product a b) c) ->
inc x (product a b) ->
W (Q x) (W (P x) (W f (second_partial_map a b c))) = W x f.
Proof. ir. rww spfb_W. awi H1. ee.
assert (partial_fun_axioms f). red. ee. am. exists a. exists b. tv.
awi H2. ee. assert (inc (P x) (domain (source f))). rw H3. rww product_domain.
rww spfa_W. rww spf_W. aw. rw H3. rww product_range.
Qed.
Theorem fpfa_bijective: forall a b c,
nonempty a -> nonempty b -> bijective (first_partial_map a b c).
Proof. ir.
assert (Ha:source (first_partial_map a b c) =
set_of_functions (product a b) c). uf first_partial_map. aw.
red. ee. red. ee. app fpfb_function. ir. rwi Ha H1; rwi Ha H2.
cp H1; cp H2. awi H1. awi H2. ee.
app function_exten. ir. ue. ue. ir. rwi H8 H10.
wr (fpfb_WW H H0 H4 H10). wr (fpfb_WW H H0 H5 H10). rww H3.
app surjective_pr6. app fpfb_function. ir.
assert (Hb:target (first_partial_map a b c) =
set_of_functions b (set_of_functions a c)). uf first_partial_map. aw.
rwi Hb H1. cp H1. awi H1. ee.
set (f:= BL (fun x => W (P x) (W (Q x) y)) (product a b) c).
assert (transf_axioms (fun x : Set => W (P x) (W (Q x) y)) (product a b) c).
red. ir. awi H5. ee. assert (inc (W (Q c0) y) (target y)).
app inc_W_target. ue. rwi H4 H8. awi H8. ee. wr H10. app inc_W_target. ue.
assert (inc f (source (first_partial_map a b c))).
uf first_partial_map. aw. uf f; ee; aw; app bl_function.
ex_tac. set (g := W f (first_partial_map a b c)).
assert (inc g (target(first_partial_map a b c))). uf g. ap inc_W_target.
app fpfb_function. am. ufi first_partial_map H7. awi H7. ee.
app function_exten. ue. ue. ir.
assert (inc (W x g) (target g)). app inc_W_target. rwi H9 H11.
assert (inc (W x y) (set_of_functions a c)). wr H4. app inc_W_target. ue. ue.
awi H12. awi H11. ee. app function_exten. ue. ue. ir.
rwi H15 H17. uf g. assert (inc (J x0 x) (source f)). uf f. aw. eee.
ufi first_partial_map H6. rwi bl_source H6. cp H6. awi H19. ee. rwi H20 H18.
cp (fpfb_WW H H0 H6 H18). awi H22. rw H22. uf f. rww bl_W. aw.
Qed.
Theorem spfa_bijective: forall a b c,
nonempty a -> nonempty b -> bijective (second_partial_map a b c).
Proof. ir.
assert (Ha:source (second_partial_map a b c) =
set_of_functions (product a b) c). uf second_partial_map. aw.
red. ee. red. ee. app spfb_function. ir. rwi Ha H1; rwi Ha H2.
cp H1; cp H2. awi H1. awi H2. ee.
app function_exten. ir. ue. ue. ir. rwi H8 H10.
wr (spfb_WW H H0 H4 H10). wr (spfb_WW H H0 H5 H10). rww H3.
app surjective_pr6. app spfb_function. ir.
assert (Hb:target (second_partial_map a b c) =
set_of_functions a (set_of_functions b c)). uf second_partial_map. aw.
rwi Hb H1. cp H1. awi H1. ee.
set (f:= BL (fun x => W (Q x) (W (P x) y)) (product a b) c).
assert (transf_axioms (fun x : Set => W (Q x) (W (P x) y)) (product a b) c).
red. ir. awi H5. ee. assert (inc (W (P c0) y) (target y)).
app inc_W_target. ue. rwi H4 H8. awi H8. ee. wr H10. app inc_W_target. ue.
assert (inc f (source (second_partial_map a b c))).
uf second_partial_map. aw. uf f; ee; aw; app bl_function.
ex_tac. set (g := W f (second_partial_map a b c)).
assert (inc g (target(second_partial_map a b c))). uf g. ap inc_W_target.
app spfb_function. am. ufi second_partial_map H7. awi H7. ee.
app function_exten. ue. ue. ir.
assert (inc (W x g) (target g)). app inc_W_target. rwi H9 H11.
assert (inc (W x y) (set_of_functions b c)). wr H4. app inc_W_target. ue. ue.
awi H12. awi H11. ee. app function_exten. ue. ue. ir.
rwi H15 H17. uf g. assert (inc (J x x0) (source f)). uf f. aw. eee.
ufi second_partial_map H6. rwi bl_source H6. cp H6. awi H19. ee. rwi H20 H18.
cp (spfb_WW H H0 H6 H18). awi H22. rw H22. uf f. rww bl_W. aw.
Qed.
End Bunion.
Export Bunion.
Module Bproduct.
We may need the graph of a function of type
a->Set
Definition gbcreate (a:Set) (f:a->Set) := (IM (fun y:a => J (Ro y) (f y))).
Lemma gbcreate_rw: forall (a:Set) (f:a->Set) x,
inc x (gbcreate f) = exists y:a, J (Ro y) (f y) =x.
Proof. ir. uf gbcreate. app iff_eq. ir. cp (IM_exists H). simpl in H0. am.
ir. app IM_inc.
Qed.
Lemma gbcreate_graph: forall (a:Set) (f:a-> Set), is_graph (gbcreate f).
Proof. ir. red. ir. rwi gbcreate_rw H. nin H. wr H. fprops.
Qed.
Lemma gbcreate_fgraph: forall (a:Set) (f:a-> Set), fgraph (gbcreate f).
Proof. ir. red. ee. app gbcreate_graph. ir. rwi gbcreate_rw H.
rwi gbcreate_rw H0. nin H. nin H0. wri H H1; wri H0 H1. awi H1.
cp (R_inj H1). wr H0; wr H; ue. ue.
Qed.
Lemma gbcreate_domain : forall (a:Set) (f:a-> Set),
domain (gbcreate f) = a.
Proof. ir. set_extens. awi H. nin H. rwi gbcreate_rw H. nin H.
wr (pr1_def H). app R_inc. app gbcreate_graph. aw.
exists (f (Bo H)). rw gbcreate_rw. exists (Bo H). rww (B_eq H).
app gbcreate_graph.
Qed.
Lemma gbcreate_V : forall (a:Set) (f:a-> Set) (x:a),
V (Ro x) (gbcreate f) = f x.
Proof. ir. assert (inc (J (Ro x) (f x)) (gbcreate f)). rw gbcreate_rw.
exists x. tv. set (pr2_V (gbcreate_fgraph f) H). sy. awii e.
Qed.
We have three equivalent definitions of the product; in any case,
an element of the product is a functional graph with fixed domain
Definition productb f:=
Zo (powerset (product (domain f) (unionb f)))
(fun z => fgraph z & domain z = domain f
& forall i, inc i (domain f) -> inc (V i z) (V i f)).
Definition productt (I:Set) (f:I->Set):= productb (gbcreate f).
Definition productf sf f:= productb (L sf f).
Lemma productb_rw: forall f x,
fgraph f ->
inc x (productb f) =
(fgraph x & domain x = domain f &
forall i, inc i (domain x) -> inc (V i x) (V i f)).
Proof. ir. uf productb. ap iff_eq. ir. Ztac. eee.
ir. ee. wr H1. Ztac. aw. red. ir. assert (is_graph x). fprops. cp (H4 _ H3).
assert (exists y : Set, inc (J (P x0) y) x). exists (Q x0). aw. aw. eee.
assert (inc (P x0) (domain x)). aw. cp (H2 _ H7). rw (pr2_V H0 H3).
union_tac. ue.
Qed.
Lemma productt_rw: forall (I:Set) (f:I->Set) x,
inc x (productt f) =
(fgraph x & domain x = I & forall i:I, inc (V (Ro i) x) (f i)).
Proof. ir. uf productt. rw productb_rw. ap iff_eq. ir. ee. am.
rwi gbcreate_domain H0. am. rwi gbcreate_domain H0. rwi H0 H1. ir.
assert (inc (Ro i) I). app R_inc. cp (H1 _ H2). rwi gbcreate_V H3. am.
ir. ee. am. rw gbcreate_domain. am. ir. rwi H0 H2. set (y:= Bo H2).
assert (Ro y =i). uf y. app B_eq. wr H3. rw gbcreate_V. app H1.
app gbcreate_fgraph.
Qed.
Lemma productf_rw: forall sf f x,
inc x (productf sf f) =
(fgraph x & domain x = sf &
forall i, inc i (domain x) -> inc (V i x) (f i)).
Proof. ir. uf productf. rw productb_rw. bw. app iff_eq; ir; eee;ir.
set (H1 _ H2). bwi i0. am. ue. bw. app H1. ue. gprops.
Qed.
Hint Rewrite productf_rw productt_rw productb_rw: aw.
Lemma productt_exten: forall (I:Set) (f:I->Set) x x',
inc x (productt f) -> inc x' (productt f) ->
(forall i:I, V (Ro i) x = V (Ro i) x') ->
x = x'.
Proof. intros I f x x'. aw. ir. ee.
app fgraph_exten. ue. rw H4. ir. wr (B_eq H6). app H1.
Qed.
Lemma productb_exten: forall f x x',
fgraph f ->
inc x (productb f) -> inc x' (productb f) ->
(forall i, inc i (domain f) -> V i x = V i x') ->
x = x'.
Proof. intros f x x' H. aw. ir. ee. app fgraph_exten; ue.
Qed.
Lemma productf_exten: forall sf f x x',
inc x (productf sf f) -> inc x' (productf sf f) ->
(forall i, inc i sf -> V i x = V i x') ->
x = x'.
Proof. uf productf. ir. assert (fgraph (L sf f)). gprops.
app (productb_exten H2 H H0). bw.
Qed.
Lemma trivial_fgraph: forall f, L emptyset f = emptyset.
Proof. ir. uf L. set_extens. awi H. nin H. ee. elim (emptyset_pr H).
elim (emptyset_pr H).
Qed.
Projection function to component i
Definition pr_i f i:= BL(V i) (productb f) (V i f).
Definition pr_it (I:Set) (f:I ->Set):= pr_i (gbcreate f).
Lemma pri_axioms: forall f i,
fgraph f -> inc i (domain f) ->
transf_axioms (V i)(productb f)(V i f).
Proof. ir. uf pr_i. red. ir. awi H1. ee. app H3. ue. am.
Qed.
Lemma pri_function: forall f i,
fgraph f -> inc i (domain f) ->
is_function (pr_i f i).
Proof. ir. uf pr_i. app bl_function. app pri_axioms.
Qed.
Lemma pri_W: forall f i x,
fgraph f -> inc i (domain f) -> inc x (productb f) ->
W x (pr_i f i) = V i x.
Proof. ir. uf pr_i. aw. app pri_axioms.
Qed.
Hint Resolve pri_function : fprops.
Special case where the domain is empty
Lemma product_trivial :
productb emptyset = singleton emptyset.
Proof. set emptyset_fgraph.
set_extens; awi H; aw. ee. srwi H0. wrr empty_graph1. fprops.
eee. rw H. srw. ir. elim (emptyset_pr H0).
Qed.
Lemma product2_trivial: forall f,
productb (L emptyset f) = singleton emptyset.
Proof. ir. rw trivial_fgraph. app product_trivial.
Qed.
a product is empty iff all factors are empty
Lemma product_nonempty: forall f,
fgraph f -> (forall i, inc i (domain f) -> nonempty (V i f)) ->
nonempty (productb f).
Proof. ir. exists (L(domain f)(fun i=> rep (V i f))). aw.
ee. gprops. bw. bw. ir. bw. app nonempty_rep. app H0.
Qed.
Lemma product_nonempty2: forall f,
fgraph f -> nonempty (productb f) ->
(forall i, inc i (domain f) -> nonempty (V i f)).
Proof. ir. nin H0. awi H0. ee. wri H2 H1. cp (H3 _ H1). ex_tac. am.
Qed.
Lemma productt_nonempty: forall (I:Set) (f:I->Set),
(forall i, nonempty (f i)) -> nonempty (productt f).
Proof. ir. uf productt. app product_nonempty. app gbcreate_fgraph.
rw gbcreate_domain. ir. assert (i= (Ro (Bo H0))). rww B_eq. rw H1.
rw gbcreate_V. app H.
Qed.
Lemma productt_nonempty2: forall (I:Set) (f:I->Set),
nonempty (productt f) -> (forall i, nonempty (f i)).
Proof. ir. nin H. awi H. ee. exists (V (Ro i) y). app H1.
Qed.
The set of graphs is a product
Lemma graphset_pr1: forall a b z,
inc z (set_of_gfunctions a b) =
(fgraph z & domain z = a & sub z (product a b)).
Proof. ir. uf set_of_gfunctions. app iff_eq. ir. Ztac. awi H0. eee.
ir. eee. Ztac. aw.
Qed.
Lemma graphset_pr2: forall a b z,
inc z (set_of_gfunctions a b) =
(fgraph z & domain z = a & sub (range z) b).
Proof. ir. rw graphset_pr1. app iff_eq. ir. eee.
assert (corr_propb a b z). red. eee. rwi corr_propc H2. eee.
ir. eee. assert (corr_propb a b z). rw corr_propc. eee. red in H2. am.
Qed.
Lemma product_sub_graphset: forall f x,
fgraph f -> sub (unionb f) x ->
sub (productb f) (set_of_gfunctions (domain f) x).
Proof. ir. red. ir. awii H1. ee. rw graphset_pr2. ee.
am. am. red. ir. srwi H4. nin H4. ee. rw H5. app H0.
apply unionb_inc with x2. wrr H2. app H3. am.
Qed.
Lemma product_eq_graphset: forall f x,
fgraph f -> (forall i, inc i(domain f) -> V i f = x) ->
productb f = set_of_gfunctions (domain f) x.
Proof. ir. app extensionality. app product_sub_graphset. red. ir.
cp (unionb_exists H1). nin H2. ee. rwi H0 H3. am. am.
red. ir. rwi graphset_pr2 H1. aw. eee. ir.
rw H0. app H3. fprops. ue.
Qed.
Product of a single set
Definition product1 (x a:Set) := productt (fun _:singleton a => x).
Lemma product1_pr: forall x a,
product1 x a = set_of_gfunctions (singleton a) x.
Proof. ir. uf product1. uf productt.
set (gbcreate_fgraph (fun _ : singleton a => x)).
rw (product_eq_graphset f (x:=x)). rww gbcreate_domain.
rw gbcreate_domain. ir. wr (B_eq H). rww gbcreate_V.
Qed.
Lemma product1_pr2: forall f x, fgraph f -> domain f = singleton x ->
product1 (V x f) x = productb f.
Proof. ir. cut (gbcreate (fun _ : singleton x => V x f) = f). ir.
uf product1. uf productt. rww H1.
app fgraph_exten. app gbcreate_fgraph. rw gbcreate_domain. sy; am.
rw gbcreate_domain. ir. wr (B_eq H1). rw gbcreate_V. rw (B_eq H1). awi H1. ue.
Qed.
Lemma product1_rw: forall x a y,
inc y (product1 x a) = (fgraph y & domain y = singleton a
& inc (V a y) x).
Proof. ir. rw product1_pr. rw graphset_pr2.
app iff_eq. ir. eee. app H1. app inc_V_range. rw H0. app singleton_inc.
ir. eee. red. ir. srwi H2. nin H2. ee. rwi H0 H2. awi H2. ue. ue. am.
Qed.
Definition product1_canon x a :=
BL (fun i : Set => L(singleton a) (fun _ : Set => i))
x (product1 x a).
Lemma product1_canon_axioms: forall x a,
transf_axioms (fun i => L(singleton a) (fun _ :Set => i)) x (product1 x a).
Proof. ir. red. ir. rw product1_rw. ee. gprops. bw. bw. fprops.
Qed.
Lemma product1_canon_function: forall x a,
is_function (product1_canon x a).
Proof. ir. uf product1_canon. app bl_function. app product1_canon_axioms.
Qed.
Lemma product1_canon_W: forall x a i,
inc i x -> W i (product1_canon x a) =
L(singleton a) (fun _ : Set => i).
Proof. ir. uf product1_canon. aw. app product1_canon_axioms.
Qed.
Lemma product1_canon_bijective: forall x a,
bijective(product1_canon x a).
Proof. ir. uf product1_canon. app bl_bijective.
app product1_canon_axioms. ir. cp (f_equal (V a) H1). simpl in H2. bwi H2.
am. fprops. fprops.
ir. rwi product1_rw H. ee. ex_tac. wr H0.
ap fgraph_exten. gprops. am. bw. bw. rw H0. ir. bw. db_tac.
Qed.
A product of n sets (with n=2) is isomorphic to the product of two sets
Definition product2 x y :=
productf two_points (variant TPa x y).
Definition product2_canon x y :=
BL (fun z => (variantLc (P z) (Q z))) (product x y) (product2 x y).
Lemma variant_if_rw1: forall x y, variant TPa x y TPa = x.
Proof. ir. rw variant_if_rw. tv. tv. Qed.
Lemma variant_if_not_rw1: forall x y, variant TPa x y TPb = y.
Proof. ir. rw variant_if_not_rw. tv. ap two_points_distinctb. Qed.
Hint Rewrite variant_if_not_rw1 variant_if_rw1 : bw.
Ltac try_lvariant u:= rwi two_points_pr u; nin u; rw u; bw.
Lemma product2_rw: forall x y z,
inc z (product2 x y) = (fgraph z & domain z = two_points &
inc (V TPa z) x &
inc (V TPb z) y).
Proof. ir. uf product2. aw. app iff_eq. ir. eee.
assert (inc TPa (domain z)). rw H0. fprops. cp (H1 _ H2). bwi H3. am.
assert (inc TPb (domain z)). rw H0. fprops. cp (H1 _ H2). bwi H3. am.
ir. eee. ir. rwi H0 H3. try_lvariant H3.
Qed.
Lemma product2_canon_axioms: forall x y,
transf_axioms (fun z => variantLc (P z) (Q z))
(product x y) (product2 x y).
Proof. red. ir. rw product2_rw. ee. aw. aw. tv. fprops. bw. bw. awi H.
ee. am. bw. awi H; eee.
Qed.
Lemma product2_canon_function: forall x y,
is_function (product2_canon x y).
Proof. ir. uf product2_canon. app bl_function.
app product2_canon_axioms.
Qed.
Lemma product2_canon_W: forall x y z,
inc z (product x y) -> W z (product2_canon x y) = variantLc (P z) (Q z).
Proof. ir. uf product2_canon. bw. awi H. aw. app product2_canon_axioms.
Qed.
Lemma product2_canon_bijective: forall x y,
bijective (product2_canon x y).
Proof. ir. set (product2_canon_axioms (x:=x) (y:=y)).
uf product2_canon. app bl_bijective.
ir. awi H; awi H0. ee. set (f_equal (V TPa) H1). bwi e.
set (f_equal (V TPb) H1). bwi e0. app pair_extensionality.
ir. rwi product2_rw H. ee. exists (J (V TPa y0) (V TPb y0)). split.
fprops. aw. sy. ap fgraph_exten. am. fprops. bw. rw H0.
ir. try_lvariant H3.
Qed.
The product of singletons is a singleton
Definition is_singleton x := exists u, x = singleton u.
Lemma is_singleton_rw: forall x,
is_singleton x = (nonempty x & (forall a b, inc a x -> inc b x -> a = b)).
Proof. ir. app iff_eq. ir. nin H. ee. rw H. exists x0. fprops.
ir. rwi H H0. rwi H H1. awi H0. awi H1. ue.
ir. ee. nin H. exists y. set_extens. rw (H0 _ _ H1 H). fprops. db_tac.
Qed.
Lemma product_singleton: forall f,
fgraph f -> (forall i, inc i (domain f) -> is_singleton (V i f))
-> is_singleton (productb f).
Proof. ir. rw is_singleton_rw. ee. app product_nonempty. ir. set (H0 _ H1).
rwi is_singleton_rw i0. ee. am. ir. ap (productb_exten H H1 H2).
ir. set (H0 _ H3). rwi is_singleton_rw i0. awii H1; awii H2. ee. app H5.
app H9. ue. app H7. ue.
Qed.
Some properties of constant graphs
Definition constant_graph s x :=
L s (fun _ => x).
Definition is_constant_graph f :=
fgraph f &
(forall x x', inc x (domain f) -> inc x' (domain f) -> V x f = V x' f).
Lemma constant_graph_function: forall f,
is_constant_function f -> is_constant_graph(graph f).
Proof. ir. red in H. red. ee. fprops. ufi W H0. red in H. ee. ue.
Qed.
Lemma constant_graph_V: forall s x y,
inc y s -> V y (constant_graph s x) = x.
Proof. ir. uf constant_graph. bw.
Qed.
Lemma constant_graph_small_range: forall f,
is_constant_graph f -> small_set(range f).
Proof. ir. red. red in H. ir. ee. srwi H0. srwi H1.
nin H0; nin H1. ee. set (H2 _ _ H0 H1). ue. ue. am. am.
Qed.
Definition diagonal_graphp e i :=
Zo(set_of_gfunctions i e) is_constant_graph.
Lemma diagonal_graph_rw: forall e i x,
inc x (diagonal_graphp e i) =
(is_constant_graph x & domain x = i & sub (range x) e).
Proof. ir. uf diagonal_graphp. app iff_eq. ir. Ztac.
rwi graphset_pr2 H0. eee.
ir. ee. Ztac. rw graphset_pr2. red in H. intuition.
Qed.
Lemma constant_graph_is_constant: forall x y,
is_constant_graph(constant_graph x y).
Proof. ir. red. uf constant_graph. aw. ee. gprops. bw. ir. bw.
Qed.
Definition constant_functor i e:=
BL(fun x => constant_graph i x) e (set_of_gfunctions i e).
Lemma cf_injective : forall i e,
nonempty i -> injective (constant_functor i e).
Proof. ir. uf constant_functor. ap bl_injective.
red. ir. rw graphset_pr2. uf constant_graph. bw. ee. gprops. tv.
red. ir. bwi H1. nin H1. ee. wrr H2.
ir. nin H. transitivity (V y (constant_graph i u)). sy; app constant_graph_V.
rw H2. app constant_graph_V.
Qed.
Change of variables in a product
Definition product_compose f u :=
BL (fun x => compose_graph x (graph u))
(productb f) (productf (source u) (fun k => V (W k u) f)).
Lemma compose_V: forall u v x,
fgraph u -> fgraph v -> fgraph (compose_graph u v) ->
inc x (domain (compose_graph u v)) ->
V x (compose_graph u v) = V (V x v) u.
Proof. ir. set (fdomain_pr1 H1 H2).
set (z:= V x (compose_graph u v)). fold z in i.
awi i. nin i. nin H4. nin H4. set (pr2_V H0 H4). awi e. wr e.
set (pr2_V H H5). awi e0. am.
Qed.
Lemma pc_axioms0: forall f u c,
fgraph f -> bijective u -> target u = domain f ->
inc c (productb f) ->
let g:= compose (corresp (domain c) (range c) c) u in
is_function g & compose_graph c (graph u) = graph g &
(forall i, inc i (source u) ->
V i (graph g) = V (V i (graph u)) c).
Proof. ir. assert (is_function u). fct_tac. awii H2.
assert (compose_graph c (graph u) = graph g). uf g. uf compose. aw.
assert (is_function g). uf g. fct_tac.
app is_function_pr. fprops. aw. ue. eee.
ir. uf g. uf compose. aw. rww compose_V. fprops. ue. fprops. rw H4.
aw. uf g. aw.
Qed.
Lemma pc_axioms: forall f u,
fgraph f -> bijective u -> target u = domain f ->
transf_axioms (fun x => compose_graph x (graph u))
(productb f) (productf (source u) (fun k => V (W k u) f)).
Proof. ir. red. ir. nin (pc_axioms0 H H0 H1 H2). nin H4. rw H4. awi H2. ee.
assert (is_function u). fct_tac. aw. ee. fprops. aw.
ir. awi H9. rw H5. uf W. app H7. rw H6. wr H1.
change (inc (W i u) (target u)). app inc_W_target. am. am.
Qed.
Lemma pc_function: forall f u,
fgraph f -> bijective u -> target u = domain f ->
is_function(product_compose f u).
Proof. ir. uf product_compose. app bl_function. app pc_axioms.
Qed.
Lemma pc_W: forall f u x,
fgraph f -> bijective u -> target u = domain f ->
inc x (productb f) -> W x (product_compose f u) = compose_graph x (graph u).
Proof. ir. uf product_compose. aw. aw. tv. app pc_axioms.
Qed.
Lemma pc_WV: forall f u x i,
fgraph f -> bijective u -> target u = domain f ->
inc x (productb f) -> inc i (source u) ->
V i (W x (product_compose f u)) = V (W i u) x.
Proof. ir. rww pc_W. nin (pc_axioms0 H H0 H1 H2). uf W. nin H5. ue.
Qed.
Lemma pc_bijective: forall f u, fgraph f -> bijective u -> target u =
domain f -> bijective (product_compose f u). Proof. ir. assert
(H2:=pc_function H H0 H1). cp H0. nin H0. assert (source
(product_compose f u) = productb f). uf product_compose. aw.
red. ee. red. ee. am. ir. rwi H5 H6; rwi H5 H7. app (productb_exten
H H6 H7). ir. wri H1 H9. nin (surjective_pr2 H4 H9). ee. wr H11.
wr (pc_WV H H3 H1 H6 H10). wr (pc_WV H H3 H1 H7 H10). ue. app
surjective_pr6. ir. set(ff:= L (source u) (fun k => V (W k u) f)).
assert (Ha:target (product_compose f u) = productb ff). uf
product_compose. aw. assert (Hb: inc y (productb ff)). ue. ufi
product_compose H6. awi H6. set (x:= L (domain f) (fun i => V (W i
(inverse_fun u)) y)). assert (inc x (productb f)). aw. uf
x. ee. gprops. bw. bw. ir. bw. wri H1 H9. nin (surjective_pr2 H4
H9). ee. wr (W_inverse2 H3 H10 (sym_eq H11)). wr H11. app H8. ue.
set H7. wri H5 i. ex_tac. set (inc_W_target H2 i). rwi Ha i0.
assert (fgraph ff). uf ff. gprops. app (productb_exten H8 i0 Hb).
ir. ufi ff H9. bwi H9. rww pc_WV. uf x. bw. wrr (W_inverse2 H3 H9
(refl_equal (W i1 u))). wr H1. app inc_W_target. fct_tac. Qed.
a partial product is the set of restrictions
Lemma graph_exten: forall r r',
is_graph r -> is_graph r' ->
(r = r') = forall u v, related r u v = related r' u v.
Proof. ir. app iff_eq. ir. ue. uf related. ir.
set_extens. assert (J (P x) (Q x) =x). aw. app H.
wr H3. wr H1. rw H3. am. assert (J (P x) (Q x) =x). aw. app H0.
wr H3. rw H1. ue.
Qed.
Lemma restriction_graph2 : forall f j,
fgraph f -> sub j (domain f) ->
L j (fun x => V x f) = compose_graph f (identity_g j).
Proof. ir. rw restr_to_domain2.
rw graph_exten. ir. rw compose_related.
uf related. aw. app iff_eq. ir. ee. exists u. aw. eee.
ir. nin H1. awi H1. eee. fprops. fprops. am. am.
Qed.
Product of f, with indices restricted to j
Definition restriction_product f j := productb (restr f j).
Definition pr_j f j :=
BL (fun z => restr z j) (productb f)(restriction_product f j).
Lemma prj_axioms: forall f j,
fgraph f -> sub j (domain f) ->
transf_axioms (fun z => restr z j)
(productb f)(restriction_product f j).
Proof. ir. red. ir. awi H1. ee. uf restriction_product.
wrr restr_to_domain2. aw. bw. eee. gprops. sy. app restr_domain1.
ir. bw. app H3. rw H2. app H0. fprops. ue. am.
Qed.
Lemma prj_function: forall f j,
fgraph f -> sub j (domain f) -> is_function (pr_j f j).
Proof. ir. uf pr_j. app bl_function. app prj_axioms.
Qed.
Lemma prj_W: forall f j x,
fgraph f -> sub j (domain f) -> inc x (productb f)
-> W x (pr_j f j) = (restr x j).
Proof. ir. uf pr_j. aw. app prj_axioms.
Qed.
Lemma prj_WV: forall f j x i,
fgraph f -> sub j (domain f) -> inc x (productb f) -> inc i j
-> V i (W x (pr_j f j)) = V i x.
Proof. ir. rww prj_W. uf pr_j. awi H1. ee. bw; ue. am.
Qed.
Lemma extension_partial_product: forall f j g,
fgraph f -> (forall i, inc i (domain f) -> nonempty (V i f)) ->
fgraph g -> domain g = j -> sub j (domain f) ->
(forall i, inc i j -> inc (V i g) (V i f)) ->
exists h, domain h = domain f &
fgraph h & (forall i, inc i (domain f) -> inc (V i h) (V i f)) &
(forall i, inc i j -> V i h = V i g).
Proof. ir. set (h:= union2 g (unionf (complement (domain f) j)
(fun i => (singleton (J i (rep (V i f))))))).
assert (is_graph h). red. ir. ufi h H5. nin (union2_or H5).
red in H1. ee. app H1. nin (unionf_exists H6). nin H7. db_tac.
assert (domain h = domain f). set_extens. awi H6. nin H6.
ufi h H6. nin (union2_or H6). app H3. wr H2. aw. ex_tac. fprops.
nin (unionf_exists H7). nin H8. awi H9. wri (pr1_def H9) H8. srwi H8; eee. am.
aw. nin (inc_or_not x j). wri H2 H7. awi H7. nin H7. exists x0. uf h.
inter2tac. fprops. assert (inc x (complement (domain f) j)). srw. intuition.
exists (rep (V x f)). uf h. app union2_second. union_tac.
assert (fgraph h). red. ee. am. ir.
ufi h H7. cp (union2_or H7). ufi h H8. cp (union2_or H8). nin H10.
nin H11. red in H1. ee. app (H12 _ _ H10 H11 H9). nin (unionf_exists H11).
ee. awi H13. cp (inc_pr1_domain H10). rwi H2 H14. rwi H9 H14. rwi H13 H14.
awi H14. srwi H12. ee. contradiction.
nin (unionf_exists H10). ee. awi H13. nin H11.
cp (inc_pr1_domain H11). rwi H2 H14. wri H9 H14. rwi H13 H14.
awi H14. srwi H12. ee. contradiction.
nin (unionf_exists H11). ee. awi H15. rwi H13 H9; rwi H15 H9. awi H9.
rwi H9 H13. ue.
assert (forall i, inc i j -> V i h = V i g). ir.
assert (sub g h). uf h. red. ir. inter2tac.
wri H2 H8. sy. app (sub_graph_ev H7 H9 H8).
exists h. eee. ir. nin (inc_or_not i j). ir. rw H8. app H4.
am. ir. assert (inc i (complement (domain f) j)). srw.
intuition. assert (inc (J i (rep (V i f))) h). uf h. app union2_second.
union_tac. fprops. cp (pr2_V H7 H12). awi H13.
wr H13. app nonempty_rep. app H0.
Qed.
Lemma prj_surjective: forall f j,
fgraph f -> (forall i, inc i (domain f) -> nonempty (V i f)) ->
sub j (domain f) -> surjective (pr_j f j).
Proof. ir. app surjective_pr6. app prj_function. uf pr_j. aw.
ir. cp H2. ufi restriction_product H2. awi H2. ee.
wri restr_to_domain2 H4; tv. bwi H4.
assert (forall i, inc i j -> inc (V i y) (V i f)). ir.
rwi H4 H5. cp (H5 _ H6). bwi H7; am.
nin (extension_partial_product H H0 H2 H4 H1 H6). ee.
assert (inc x (productb f)). aw. rw H7. intuition.
ex_tac. sy. change (y = W x (pr_j f j)). rww prj_W.
app fgraph_exten. fprops. rww restr_domain1. ue. ir. bw. sy;app H10. ue. ue.
ue. fprops.
Qed.
Lemma pri_surjective: forall f k,
fgraph f -> (forall i, inc i (domain f) -> nonempty (V i f)) ->
inc k (domain f) -> surjective (pr_i f k).
Proof. ir. set (j:= singleton k).
assert (sub j (domain f)). red. ir. ufi j H2. db_tac.
assert (composable (product1_canon (V k f) k) (pr_i f k)). red. ir.
ee. app product1_canon_function. app pri_function.
uf product1_canon. uf pr_i. aw.
assert (is_function (compose (product1_canon (V k f) k) (pr_i f k))).
fct_tac. assert (pr_j f j = compose (product1_canon (V k f) k) (pr_i f k)).
ap function_exten. app prj_function. am.
uf pr_j. uf pr_i. aw. uf pr_j; uf pr_i. aw.
uf product1_canon. aw. uf product1.
assert(restr f j = L (singleton k) (fun _ : Set => V k f)). uf j.
app fgraph_exten. fprops. gprops. bw. rww restr_domain1.
ir. rwi restr_domain1 H5. rww (singleton_eq H5). bw. bw. fprops. fprops.
am. fprops. uf restriction_product. ue. ir.
cp H5. ufi pr_j H5. awi H5.
aw. rw product1_canon_W. rww prj_W. ee.
app fgraph_exten. fprops. gprops. bw. rww restr_domain1. ue.
ir. rwi restr_domain1 H9. bw. rww pri_W.
ufi j H9. rww (singleton_eq H9). aw; eee. ue. am. ue. aw; eee.
assert (target (pr_i f k) = V k f). uf pr_i. aw. wr H7. app inc_W_target.
app pri_function. uf pr_i. aw. uf pr_i. aw. am. app (surj_left_compose2 H3).
wr H5. app prj_surjective. nin (product1_canon_bijective (V k f) k). am.
Qed.
Lemma productb_monotone1: forall f g,
fgraph f -> fgraph g -> domain f = domain g ->
(forall i, inc i (domain f) -> sub (V i f) (V i g))
-> sub (productb f) (productb g).
Proof. ir. red. ir. awi H3. ee. aw. eee.
ir. wri H4 H2. app H2. app H5. am.
Qed.
Lemma productb_monotone2: forall f g,
fgraph f -> fgraph g -> domain f = domain g ->
(forall i, inc i (domain f) -> nonempty (V i f)) ->
sub (productb f) (productb g) ->
(forall i, inc i (domain f) -> sub (V i f) (V i g)).
Proof. ir. red. ir. assert (inc x (target (pr_i f i))). uf pr_i. aw.
nin (surjective_pr2 (pri_surjective H H2 H4) H6). nin H7.
ufi pr_i H7. rwi bl_source H7. wr H8. rww pri_W. set (H3 _ H7).
awii i0. ee. app H11. rw H10. ue.
Qed.
Given a product with domain I, and a partition J of I, we can consider the
set of mappings that associate to each j in J the partial product.
This is a product. Associativity says that this product of products
is isomorphic to the initial product.
Implies associativity of cardinal product
Definition prod_assoc_axioms f g :=
fgraph f & partition_fam g (domain f).
Definition prod_assoc_map f g :=
BL(fun z => (L (domain g) (fun l => W z (pr_j f (V l g)))))
(productb f)
(productf (domain g) (fun l => (restriction_product f (V l g)))).
Lemma pam_axioms: forall f g,
prod_assoc_axioms f g ->
transf_axioms(fun z => (L (domain g) (fun l => W z (pr_j f (V l g)))))
(productb f)
(productf (domain g) (fun l => (restriction_product f (V l g)))).
Proof. ir. red. red in H. ee. ir. aw. ee. gprops. bw.
bw. ir. bw. assert (restriction_product f (V i g) = target (pr_j f (V i g))).
uf pr_j. aw. rw H3. app inc_W_target. app prj_function. red in H0. ee.
wr H5. red. ir. union_tac. uf pr_j. rww bl_source.
Qed.
Lemma pam_function: forall f g,
prod_assoc_axioms f g ->
is_function (prod_assoc_map f g).
Proof. ir. uf prod_assoc_map. app bl_function. app pam_axioms. Qed.
Lemma pam_W: forall f g x,
prod_assoc_axioms f g -> inc x (productb f) ->
W x (prod_assoc_map f g) = (L (domain g) (fun l => W x (pr_j f (V l g)))).
Proof. ir. uf prod_assoc_map. aw. app pam_axioms.
Qed.
Lemma pam_injective: forall f g,
prod_assoc_axioms f g ->
injective(prod_assoc_map f g).
Proof. ir. split. app pam_function. set H. nin p;ee.
assert (source (prod_assoc_map f g) = productb f). uf prod_assoc_map. aw.
rw H2. ir. app (@productb_exten _ x y H0).
do 2 rwii pam_W H5. ir. red in H1. ee. wri H8 H6. nin (unionb_exists H6). ee.
assert (sub (V x0 g) (domain f)). red. ir. wr H8. ap (unionb_inc H9 H11).
set (f_equal (V x0) H5). bwi e; tv. rwii prj_W e. rwii prj_W e.
set (f_equal (V i) e). awii H3. awii H4. ee. bwi e0; tv. ue. ue.
Qed.
Theorem pam_bijective: forall f g,
prod_assoc_axioms f g ->
bijective(prod_assoc_map f g).
Proof. ir. split. app pam_injective. app surjective_pr6. app pam_function.
assert (Hb:= H). nin H. assert (Hc:= H0). red in H0. ee.
ir. ufi prod_assoc_map H3. rwi bl_target H3. set H3. awi i. ee.
assert (Ht: source (prod_assoc_map f g) = productb f).
uf prod_assoc_map. aw. rw Ht.
assert (Hd: forall i, inc i (domain g) -> sub (V i g) (domain f)).
wr H2. ir. red. ir. union_tac.
set (h:= fun i => BL (fun z => (V z (V i y))) (V i g) (unionb f)).
assert(Ha:forall i, inc i (domain g) ->
transf_axioms (fun z => V z (V i y)) (V i g) (unionb f)).
red. ir. assert (He:=Hd _ H7). apply unionb_inc with c. app He. wri H5 H7.
cp (H6 _ H7). ufi restriction_product H9. awi H9. ee.
wri restr_to_domain2 H10. bwi H10. rwi H10 H11. set (H11 _ H8). bwi i0. am.
am. am. am. am. am. fprops.
assert (forall i, inc i (domain g) -> function_prop (h i) (V i g) (unionb f)).
red. ir. uf h. ee. app bl_function. app Ha. aw. aw.
nin (extension_partition _ Hc H7). nin H8. clear H9. nin H8. red in H8. ee.
assert (inc (graph x) (productb f)). aw. eee.
ir. change (inc (W i x) (V i f)). rwi H10 H12. wri H2 H12.
nin (unionb_exists H12). ee. nin (H9 _ H13). ee. rww H17. uf h. aw.
wri H5 H13. cp (H6 _ H13). ufi restriction_product H18. awi H18. eee.
wri restr_to_domain2 H19. bwi H19. rwi H19 H20. set (H20 _ H14). bwi i0.
am. am. app Hd. ue. am. am. app Hd. ue. fprops. app Ha.
assert (inc (W (graph x) (prod_assoc_map f g))(target (prod_assoc_map f g))).
app inc_W_target. app pam_function. rww Ht.
ex_tac. sy.
app (productf_exten (x:=y) (x':= W (graph x) (prod_assoc_map f g)) H3).
ufi prod_assoc_map H13. rwi bl_target H13. am. ir. rww pam_W. bw.
cp (Hd _ H14). rww prj_W. wri H5 H14. cp (H6 _ H14).
ufi restriction_product H16. awi H16. ee. wri restr_to_domain2 H17. bwi H17.
assert (sub (V i g) (domain (graph x))). aw. ue.
app fgraph_exten. fprops. rww restr_domain1. fprops. rw H17. ir. bw.
change (V x0 (V i y) = W x0 x). rwi H5 H14. nin (H9 _ H14). ee. rww H23.
uf h. aw. app Ha. fprops. am. am. fprops.
Qed.
Lemma variantLc_prop: forall x y,
variantLc x y = L two_points (variant TPa x y).
Proof. uf variantLc. uf variantL. rww two_points_pr2. Qed.
Lemma prod_assoc_map2: forall f g,
prod_assoc_axioms f g -> domain g = two_points
-> equipotent (productb f)
(product (restriction_product f (V TPa g)) (restriction_product f (V TPb g))).
Proof. ir. apply equipotent_transitive with
(productf (domain g) (fun l => (restriction_product f (V l g)))).
red. exists (prod_assoc_map f g). ee. app pam_bijective.
uf prod_assoc_map. aw. uf prod_assoc_map. aw. app equipotent_symmetric.
exists (product2_canon (restriction_product f (V TPa g))
(restriction_product f (V TPb g))). ee. app product2_canon_bijective.
uf product2_canon. aw. uf product2_canon. aw. uf product2. uf productf.
app uneq. app fgraph_exten. gprops. gprops. bw. sy; am. bw. ir. bw.
try_lvariant H1. ue.
Qed.
The product of two sets is equipotent to one of them if the other one is a singleton. Implies that one is a unit for carinal product.
Lemma first_proj_bijective: forall x y,
is_singleton y -> bijective (first_proj (product x y)).
Proof. ir. assert(is_graph (product x y)). app product_is_graph.
assert (source (first_proj (product x y)) = (product x y)). uf first_proj. aw.
assert (is_function (first_proj (product x y))). app first_proj_function.
nin H. red. ee. red. ee. am. ir. rwi H1 H3. rwi H1 H4.
do 2 rwii first_proj_W H5. awi H3; awi H4. ee. rwi H H9; rwi H H7.
app pair_extensionality. rw (singleton_eq H9). db_tac. aw.
app surjective_pr6. ir. ufi first_proj H3. awi H3. nin H3.
rw H1. ex_tac. rw first_proj_W. aw. am. am.
Qed.
A product is isomophic to a partial product if missing factors are singletons. Implies that one can be removed in cardinal products.
Lemma prj_bijective: forall f j,
fgraph f -> sub j (domain f) ->
(forall i, inc i (complement (domain f) j) -> is_singleton (V i f)) ->
bijective (pr_j f j).
Proof. ir. set (k:= (complement (domain f) j)).
assert (Ht:domain (restr f (complement (domain f) j)) = k).
wr restr_to_domain2. bw. am. app sub_complement.
assert (is_singleton (restriction_product f k)).
uf restriction_product. app product_singleton. fprops. wr restr_to_domain2.
bw. ir. bw. app H1. am. uf k. app sub_complement.
set(g:= variantLc j (complement (domain f) j)).
assert (prod_assoc_axioms f g).
split. am. app (is_partition_with_complement H0).
set (f1:= prod_assoc_map f g). assert (bijective f1). uf f1.
app pam_bijective. assert (Ha:is_function f1). fct_tac.
set (xa:= restriction_product f (V TPa g)).
set (xb:= restriction_product f (V TPb g)).
set (f2:= inverse_fun (product2_canon xa xb)).
assert (domain g = two_points). uf g. bw.
assert (V TPa g = j). uf g. bw.
assert (V TPb g = k). uf g. bw.
assert (bijective f2). uf f2. ap inverse_bij_is_bij1.
ap product2_canon_bijective.
assert (Hb:is_function f2). fct_tac.
assert (source f2 = target f1). uf f1; uf f2. aw. uf product2_canon. aw.
uf prod_assoc_map. aw. uf product2. rw H5. uf productf. app uneq.
app L_exten1. ir. try_lvariant H9.
set (f3:= first_proj (product xa xb)).
assert (is_singleton xb). uf xb.
uf restriction_product. app product_singleton. fprops. bw. rw H7.
wrr restr_to_domain2. bw. ir. bw. app H1. uf k. app sub_complement.
assert (bijective f3). uf f3. app first_proj_bijective.
assert (source f3 = target f2). uf f3. uf f2. uf product2_canon.
uf first_proj. aw.
assert (composable f3 f2). red. ee. fct_tac. am. am.
assert (bijective (compose f3 f2)). app compose_bijective.
assert (composable (compose f3 f2) f1). red. eee. fct_tac. aw.
cut (pr_j f j =compose (compose f3 f2) f1). ir. rw H16. app compose_bijective.
ap function_exten. app prj_function. fct_tac. uf pr_j. uf f1.
uf prod_assoc_map. aw. uf f3. uf pr_j. uf first_proj.
rw product_domain. aw. ue. red in H10. nin H10. rw H10. fprops.
ir. ufi pr_j H16. rwi bl_source H16.
assert (Hu: inc x (source f1)). uf f1. uf prod_assoc_map. rww bl_source.
set (y:= W x f1). assert (y= W x f1). tv. ufi f1 H17. rwii pam_W H17.
set (z:= W y f2). assert (z = W y f2). tv.
assert (inc y (target f1)). uf y. app inc_W_target.
assert (inc z (target f2)). uf z. wri H9 H19. fprops.
assert (inc (J y z) (graph f2)). rw H18. graph_tac. ue.
assert (is_function (product2_canon xa xb)). app product2_canon_function.
assert (inc z (source (product2_canon xa xb))).
ufi f2 H21. ufi inverse_fun H21. awi H21. graph_tac.
assert (inc z (product xa xb)). ufi product2_canon H23. awi H23. ee. aw. eee.
assert (inc y (source f2)). graph_tac. aw. uf f3. fold y. fold z.
rww first_proj_W.
assert (P z = V TPa y). ufi f2 H21. ufi inverse_fun H21. awi H21.
cp (W_pr2 H22 H21). awi H26. rwi product2_canon_W H26. rw H26. bw. am.
rw H26. uf y. uf f1. rw pam_W. bw. rww H6. rw H5. fprops. am. am.
Qed.
Given a double family Xij, union over I of intersection over J is
intersection of union, and conversely. The new index set is a product.
Theorem distrib_union_inter: forall f,
fgraph f -> nonempty (domain f) ->
(forall l, inc l (domain f) -> fgraph (V l f)) ->
(forall l, inc l (domain f) -> nonempty (domain (V l f))) ->
unionf (domain f) (fun l => intersectionb (V l f)) =
intersectionf (productf (domain f) (fun l => (domain (V l f))))
(fun g => (unionf (domain f) (fun l => V (V l g) (V l f)))).
Proof. ir. set_extens. app intersectionf_inc. uf productf. app product_nonempty.
gprops. bw. ir. bw. app H2.
ir. nin (unionf_exists H3). awi H4. ee. union_tac.
cp (H1 _ H5). wri H7 H5. cp (H8 _ H5). ap (intersectionb_forall H6 H10).
ex_middle.
assert (nonempty (productf (domain f) (fun l =>
(Zo (domain (V l f)) (fun i => ~ (inc x (V i (V l f)))))))).
uf productf. ap product_nonempty. gprops. bw. ir. bw.
set (jl:=(Zo (domain (V i f)) (fun i0 => ~ inc x (V i0 (V i f))))).
nin (emptyset_dichot jl). elim H4. union_tac.
app intersectionb_inc. cp (H2 _ H5). nin H7. awi H7. nin H7. ex_tac.
cp (H1 _ H5). fprops.
ir. nin (inc_or_not i0 jl). rwi H6 H8. elim (emptyset_pr H8).
ufi jl H8. ex_middle. elim H8. Ztac. am. nin H5.
assert (inc y (productf (domain f) (fun l => domain (V l f)))). aw. awi H5.
eee. ir. set (H7 _ H8). Ztac. am.
set (intersectionf_forall H3 H6). nin (unionf_exists i).
ee. awi H5. ee. wri H9 H7. set (H10 _ H7). Ztac. contradiction.
Qed.
Lemma complementary_union1: forall sf f x,
nonempty sf -> (forall i, inc i sf -> sub (f i) x) ->
complement x (unionf sf f) = intersectionf sf (fun i=> complement x (f i)).
Proof. ir. uf unionf. nin H. aw. uf intersectionf. wrr complementary_union.
ir. app (H0 (Ro i)). app R_inc. nin H. app nonemptyT_intro.
Qed.
Lemma complementary_intersection1: forall sf f x,
nonempty sf -> (forall i, inc i sf -> sub (f i) x) ->
complement x (intersectionf sf f) = unionf sf (fun i=> complement x (f i)).
Proof. ir. uf unionf. nin H. uf intersectionf.
rww complementary_intersection. ir. app (H0 (Ro i)). app R_inc.
nin H. app nonemptyT_intro.
Qed.
Theorem distrib_inter_union: forall f,
fgraph f -> nonempty (domain f) ->
(forall l, inc l (domain f) -> fgraph (V l f)) ->
(forall l, inc l (domain f) -> nonempty (domain (V l f))) ->
intersectionf (domain f) (fun l => unionb (V l f)) =
unionf (productf (domain f) (fun l => (domain (V l f))))
(fun g => (intersectionf (domain f) (fun l => V (V l g) (V l f)))).
Proof. ir. set_extens.
set (yf := fun j => choose (fun a => inc a (domain (V j f))&
inc x (V a (V j f)))).
assert (forall j, inc j (domain f) -> (inc (yf j) (domain (V j f))&
inc x (V (yf j) (V j f)))). ir. uf yf. app choose_pr.
set (intersectionf_forall H3 H4). nin (unionb_exists i). exists x0. am.
apw unionf_inc (L (domain f) yf). aw. eee. gprops. bw. bw. ir. bw.
nin (H4 _ H5). am. app intersectionf_inc. ir. bw. nin (H4 _ H5). am.
app intersectionf_inc. ir. nin (unionf_exists H3). ee. awi H5.
ee. set (intersectionf_forall H6 H4). simpl in i. union_tac. app H8. ue.
Qed.
Variants of distributivity of union and intersection of Xij
when one index set has two elements
Lemma nonempty_from_domain: forall x,
nonempty (domain x) -> nonempty x.
Proof. uf domain. ir. nin H. awi H. nin H. nin H. exists x0. am.
Qed.
Lemma distrib_union2_inter: forall f g,
fgraph f -> fgraph g -> nonempty (domain f) -> nonempty (domain g) ->
union2 (intersectionb f)(intersectionb g) =
intersectionf(product (domain f)(domain g)) (fun z =>
(union2 (V (P z) f) (V (Q z) g))).
Proof. ir. assert (Ha:nonempty (product (domain f) (domain g))).
nin H1. nin H2. exists (J y y0). fprops.
set_extens. app intersectionf_inc. ir. rwi product_inc_rw H4. ee.
nin (union2_or H3). set (intersectionb_forall H7 H5). inter2tac.
set (intersectionb_forall H7 H6). inter2tac. rwi intersectionf_rw H3.
nin (inc_or_not x (intersectionb f)). inter2tac.
assert (exists z1, inc z1 (domain f) & ~ (inc x (V z1 f))).
app exists_proof. dneg. app intersectionb_inc. app nonempty_from_domain. ir.
nin (inc_or_not x (V i f)). am. elim (H5 i). au. nin H5. nin H5.
app union2_second. app intersectionb_inc. app nonempty_from_domain.
ir. assert (inc (J x0 i) (product (domain f) (domain g))). fprops.
nin (union2_or (H3 _ H8)); awi H9. contradiction. am. am.
Qed.
Lemma distrib_inter2_union: forall f g,
fgraph f -> fgraph g -> nonempty (domain f) -> nonempty (domain g) ->
intersection2 (unionb f)(unionb g) =
unionf(product (domain f)(domain g)) (fun z =>
(intersection2 (V (P z) f) (V (Q z) g))).
Proof. ir. set_extens. nin (intersection2_both H3).
nin (unionb_exists H4). nin (unionb_exists H5). ee.
apw unionf_inc (J x0 x1). fprops. aw. app intersection2_inc.
nin (unionf_exists H3). nin H4. rwi product_inc_rw H4.
nin (intersection2_both H5). ee.
app intersection2_inc. union_tac. union_tac.
Qed.
Some small lemmas
Lemma trivial_product1: forall f, productf emptyset f = singleton emptyset.
Proof. ir. uf productf. assert (L emptyset f = emptyset). empty_tac.
ufi L H. awi H. nin H. nin H. elim (emptyset_pr H). rw H.
app product_trivial.
Qed.
Lemma unionf_singleton: forall x f, unionf (singleton x) f = f x.
Proof. ir. set_extens. nin (unionf_exists H). ee.
wrr (singleton_eq H0). assert (inc x (singleton x)).
fprops. union_tac.
Qed.
Lemma intersectionf_singleton: forall x f, intersectionf (singleton x) f = f x.
Proof. ir. assert (inc x (singleton x)). fprops.
set_extens. app (intersectionf_forall H0 H). app intersectionf_inc. fprops.
ir. db_tac.
Qed.
Lemma unionf_emptyset: forall f, unionf emptyset f = emptyset.
Proof. ir. app empty_unionf.
Qed.
Lemma nonempty_product3: forall sf f i,
inc i sf -> f i = emptyset -> productf sf f = emptyset.
Proof. ir. nin (emptyset_dichot (productf sf f)). am.
nin H1. awi H1. nin H1. ee. rwi H2 H3. cp (H3 _ H). rwi H0 H4.
elim (emptyset_pr H4).
Qed.
Distributivity of product over union and intersection
Theorem distrib_prod_union: forall f,
fgraph f ->
(forall l, inc l (domain f) -> fgraph (V l f)) ->
productf (domain f) (fun l => unionb (V l f)) =
unionf (productf (domain f) (fun l => (domain (V l f))))
(fun g => (productf (domain f) (fun l => V (V l g) (V l f)))).
Proof. ir. nin (emptyset_dichot (domain f)). rw H1.
do 2 rw trivial_product1. rw unionf_singleton. rww trivial_product1.
nin (p_or_not_p
(forall l, inc l (domain f) -> nonempty (domain (V l f)))).
set_extens.
assert (nonempty (productf (domain f) (fun l =>
(Zo (domain (V l f)) (fun i => (inc (V l x) (V i (V l f)))))))).
uf productf. ap product_nonempty. gprops. bw. ir. bw.
awi H3. ee. rwi H5 H6.
cp (H6 _ H4). cp (H0 _ H4). nin (unionb_exists H7). ee.
exists x0. Ztac. bw. nin H4. awi H4. ee.
apply unionf_inc with y. aw. eee. ir. cp (H6 _ H7).
Ztac. am. awi H3. ee. aw. ee. am. am. ir.
rwi H7 H9; wri H5 H9; cp (H6 _ H9). Ztac. am. nin (unionf_exists H3).
ee. awi H5. ee. aw. eee.
ir. cp (H7 _ H8). apply unionb_inc with (V i x0).
awi H4. ee. app H11. rw H10. ue. am.
nin (p_or_not_p (exists l, inc l (domain f) & domain (V l f) = emptyset)).
nin H3. nin H3. assert (unionb (V x f) = emptyset). uf unionb. rw H4.
app unionf_emptyset.
cp (nonempty_product3 (sf:=domain f) (fun l => domain (V l f))).
simpl in H6. rw (H6 _ H3 H4).
cp (nonempty_product3 (sf:=domain f) (fun l => unionb (V l f))).
simpl in H7. rw (H7 _ H3 H5). rww unionf_emptyset.
elim H2. ir. nin (emptyset_dichot (domain (V l f))). elim H3.
ex_tac. am.
Qed.
Theorem distrib_prod_intersection: forall f,
fgraph f -> nonempty (domain f) ->
(forall l, inc l (domain f) -> fgraph (V l f)) ->
(forall l, inc l (domain f) -> nonempty (domain (V l f))) ->
productf (domain f) (fun l => intersectionb (V l f)) =
intersectionf (productf (domain f) (fun l => (domain (V l f))))
(fun g => (productf (domain f) (fun l => V (V l g) (V l f)))).
Proof. ir.
assert(nonempty (productb (L (domain f) (fun l => domain (V l f))))).
uf productf. app product_nonempty. gprops. bw. ir. bw. app H2.
set_extens. app intersectionf_inc. ir. awi H4. awi H5. aw. eee. ir.
set (H9 _ H10). app intersectionb_forall. app H7. ue. ue.
nin H3. cp (intersectionf_forall H4 H3). simpl in H5. awi H5. ee. aw. eee.
ir. app intersectionb_inc. app nonempty_from_domain. app H2. ue.
ir. assert (nonempty (productf (domain f) (fun l =>
(Zo (domain (V l f)) (fun j => l = i -> j = i0))))).
uf productf. ap product_nonempty. gprops. bw. ir. bw.
nin (equal_or_not i1 i). ir. exists i0. Ztac. ue. ir.
nin (H2 _ H10). exists y0. Ztac. ir. contradiction.
nin H10. awi H10. ee.
assert (inc y0 (productf (domain f) (fun l => domain (V l f)))).
ir. aw. eee. ir. cp (H12 _ H13). Ztac. am.
cp (intersectionf_forall H4 H13). simpl in H14. awi H14. ee. cp (H16 _ H8).
rwi H6 H8; wri H11 H8; cp (H12 _ H8). Ztac. rwi H20 H17. am. tv.
Qed.
Lemma partition_product: forall f,
fgraph f -> nonempty (domain f) ->
(forall l, inc l (domain f) -> fgraph (V l f)) ->
(forall l, inc l (domain f) -> (partition_fam (V l f) (unionb (V l f)))) ->
partition_fam(L(productf (domain f) (fun l => domain (V l f)) )
(fun g => (productf (domain f) (fun l => V (V l g) (V l f)))))
( productf (domain f) (fun l => unionb (V l f))).
Proof. ir. red. ee. gprops. red. bw. ir. bw. nin (equal_or_not i j).
left. am. right. red.
nin (emptyset_dichot (intersection2 (productf (domain f)
(fun l => V (V l i) (V l f)))
(productf (domain f) (fun l => V (V l j) (V l f))) )). am.
assert (i = j). awi H3; awi H4. ee.
app fgraph_exten. ue. ir. rwi H9 H11; rwi H9 H10; rwi H7 H8.
set (H10 _ H11). set (H8 _ H11). nin H6. nin (intersection2_both H6).
set (H2 _ H11). ufi partition_fam p. ee. red in H15.
nin (H15 _ _ i0 i1). am. red in H17. elim (emptyset_pr (x:=(V x y))). wr H17.
inter2tac. awi H12. ee. app H19. ue. awi H13. ee. app H19. ue. contradiction.
rww distrib_prod_union. uf unionb. bw.
app unionf_extensionality. ir. bw.
Qed.
Special cases when one index set has only two elements
Lemma distrib_prod2_union: forall f g,
fgraph f -> fgraph g ->
nonempty (domain f) -> nonempty (domain g) ->
product2 (unionb f)(unionb g) =
unionf(product (domain f)(domain g))
(fun z => (product2 (V (P z) f) (V (Q z) g))).
Proof. ir. uf product2. set_extens. awi H3. ee. rwi H4 H5.
assert (inc TPa two_points); fprops. assert (inc TPb two_points); fprops.
set (H5 _ H6). bwi i. set (H5 _ H7). bwi i0.
rwi unionb_rw i. rwi unionb_rw i0. nin i; nin i0. ee.
apw unionf_inc (J x0 x1). fprops. aw. eee. ir. rwi H4 H12.
try_lvariant H12. nin (unionf_exists H3). ee. awi H5. aw. eee. ir.
rwi product_inc_rw H4. ee.
cp (H7 _ H8). rwi H6 H8. try_lvariant H8; rwi H8 H11; bwi H11; union_tac.
Qed.
Lemma distrib_prod2_inter: forall f g,
fgraph f -> fgraph g ->
nonempty (domain f) -> nonempty (domain g) ->
product2 (intersectionb f)(intersectionb g)=
intersectionf(product (domain f)(domain g)) (fun z =>
(product2 (V (P z) f) (V (Q z) g))).
Proof. ir. assert (Ha:nonempty (product (domain f) (domain g))).
nin H1. nin H2. exists (J y y0). fprops. uf product2.
set_extens. awi H3. ee. rwi H4 H5. app intersectionf_inc.
ir. rwi product_inc_rw H6. aw. eee. ir. rwi H4 H9. cp (H5 _ H9).
try_lvariant H9; rwi H9 H10; bwi H10. ap (intersectionf_forall H10 H7).
ap (intersectionf_forall H10 H8).
rwii intersectionf_rw H3. nin Ha. set (H3 _ H4). awi i. aw. eee.
assert (forall i j, inc i (domain f) -> inc j (domain g) ->
(inc (V TPa x) (V i f) & inc (V TPb x) (V j g))).
ir. assert (inc (J i j) (product (domain f) (domain g))). fprops.
set (H3 _ H10). awi i0. ee. assert (inc TPa (domain x)). ue.
set (H13 _ H14). bwi i0. am. assert (inc TPb (domain x)). ue.
set (H13 _ H14). bwi i0. am.
ir. cp (H7 _ H9). rwi H6 H9. try_lvariant H9; app intersectionb_inc;
try app nonempty_from_domain. ir. nin H2. nin (H8 _ _ H11 H2). am.
nin H1. ir. nin (H8 _ _ H1 H11). am.
Qed.
Lemma distrib_product2_union: forall f g,
fgraph f -> fgraph g ->
product (unionb f)(unionb g) =
unionf(product (domain f)(domain g)) (fun z =>
(product (V (P z) f) (V (Q z) g))).
Proof. ir. cp (emptyset_dichot (domain f)). nin H1. rw H1. srw. sy.
rw empty_unionf. uf unionb. rw H1. rw unionf_emptyset. srw. tv. tv.
nin (emptyset_dichot (domain g)). rw H2. srw. rw empty_unionf.
uf unionb. rw H2. rw unionf_emptyset. srw. tv. tv.
cp (distrib_prod2_union H H0 H1 H2). ufi product2 H3.
set_extens. awi H4.
set (qx := variantLc (P x) (Q x)).
assert (inc qx (productb (variantLc (unionb f) (unionb g)))).
aw. uf qx. ee. fprops. bw. bw.
ir. try_lvariant H7. fprops.
ufi productf H3. rwi variantLc_prop H5. rwi H3 H5.
nin (unionf_exists H5). ee. union_tac.
awi H7. nin H7. ee. assert (inc TPa (domain qx)). uf qx. bw.
fprops. cp (H11 _ H12). bwi H13. ufi qx H13. bwi H13.
assert (inc TPb (domain qx)). uf qx. bw. fprops.
cp (H11 _ H14). bwi H15.
ufi qx H15. rwi variant_V_cb H15. app product_inc. fprops. tv. fprops. gprops.
cp (unionf_exists H4). nin H5. ee. awi H6. ee.
set (qx := variantLc (P x) (Q x)).
assert (inc qx (productb (variantLc (unionb f) (unionb g)))).
ufi productf H3. wri variantLc_prop H3. rw H3. union_tac. aw.
uf qx. ee. fprops. bw. bw. ir. bw. try_lvariant H9. gprops.
awi H9. nin H9. ee. rwi variantLc_domain H10.
assert (inc TPa (domain qx)). rw H10. fprops.
cp (H11 _ H12). awi H13. ufi qx H13. bwi H13.
assert (inc TPb (domain qx)). rw H10. fprops.
cp (H11 _ H14). ufi qx H15. awi H15. bwi H15. aw. eee; aw. fprops.
Qed.
Lemma distrib_product2_inter: forall f g,
fgraph f -> fgraph g -> nonempty (domain f) -> nonempty (domain g) ->
product (intersectionb f)(intersectionb g) =
intersectionf(product (domain f)(domain g)) (fun z =>
(product (V (P z) f) (V (Q z) g))).
Proof. ir. cp (distrib_prod2_inter H H0 H1 H2). ufi product2 H3.
set_extens.
set (qx := variantLc (P x) (Q x)).
assert (inc qx (productb (variantLc (intersectionb f) (intersectionb g)))).
awi H4. ee. aw. ee. uf qx. fprops. uf qx. bw. uf qx. bw. ir. try_lvariant H7.
fprops. ufi productf H3. wri variantLc_prop H3. rwi H3 H5.
app intersectionf_inc. nin H1. nin H2. exists (J y y0).
fprops. ir. cp (intersectionf_forall H5 H6). simpl in H7.
awi H7. ee. bwi H8. rwi H8 H9.
assert (inc TPa two_points). fprops. cp (H9 _ H10). ufi qx H11.
bwi H11. assert (inc TPb two_points). fprops. cp (H9 _ H12). ufi qx H13.
bwi H13. app product_inc. awi H4. ee. am. fprops. fprops. gprops.
set (qx := variantLc (P x) (Q x)).
assert (Ha:nonempty (product (domain f) (domain g))).
nin H1. nin H2. exists (J y y0). fprops.
assert (inc qx (productb (variantLc (intersectionb f) (intersectionb g)))).
ufi productf H3. rw variantLc_prop. rw H3. app intersectionf_inc. ir.
cp (intersectionf_forall H4 H5).
simpl in H6. aw. ee. uf qx. fprops. uf qx. bw. uf qx.
bw. ir. bw. try_lvariant H7; awi H6; eee. gprops.
assert (inc TPa (domain qx)). uf qx. bw. fprops.
assert (inc TPb (domain qx)). uf qx. bw. fprops.
awi H5. ee. cp (H9 _ H6). ufi qx H10. bwi H10.
cp (H9 _ H7). ufi qx H11. bwi H11. aw. nin Ha.
cp (intersectionf_forall H4 H12). simpl in H13. awi H13. eee. fprops.
Qed.
A variant of distributivity, valid if the domain of the double family is a rectangle; works only for intersection.
Theorem distrib_inter_prod: forall f sa sb,
fgraph f -> nonempty sb ->
intersectionf sb (fun k => productf sa (fun i=> V (J i k) f)) =
productf sa (fun i => intersectionf sb (fun k=> V (J i k) f)).
Proof. ir. set_extens. nin H0. cp (intersectionf_forall H1 H0). ee.
simpl in H2. awi H2. ee. aw. eee. ir. app intersectionf_inc. ex_tac.
ir. cp (intersectionf_forall H1 H6). ee. simpl in H7. awi H7. ee.
app (H9 _ H5). awi H1. ee. app intersectionf_inc. ir.
aw. eee. ir. cp (H3 _ H5). app (intersectionf_forall H6 H4).
Qed.
Lemma productf_extension : forall sf1 f1 sf2 f2,
L sf1 f1 = L sf2 f2 -> productf sf1 f1 = productf sf2 f2.
Proof. ir. uf productf. rww H.
Qed.
Lemma distrib_prod_inter2_prod: forall f g,
fgraph f -> fgraph g -> domain f = domain g ->
nonempty (domain f) ->
intersection2 (productb f) (productb g) =
productf (domain f) (fun i => intersection2 (V i f) (V i g)).
Proof. ir. set_extens. nin (intersection2_both H3). awi H4; awi H5.
aw. eee. ir. app intersection2_inc. app H9. app H7. am. am. am.
awi H3. eee. app intersection2_inc; aw; eee;ir; set (H5 _ H6); inter2tac.
Qed.
Lemma distrib_inter_prod_inter: forall f g,
fgraph f -> fgraph g -> domain f = domain g ->
nonempty (domain f) ->
product2 (intersectionb f) (intersectionb g) =
intersectionf (domain f) (fun i => product2 (V i f) (V i g)).
Proof. ir.
set (sb:= domain f). assert (Ha:inc TPa two_points). fprops.
assert (Hb:inc TPb two_points). fprops.
set (h:= L(product two_points sb)
(fun i => Yo (P i = TPa) (V (Q i) f) (V (Q i) g))).
assert (fgraph h). uf h. gprops. assert (nonempty sb). uf sb. am.
cp (distrib_inter_prod two_points H3 H4). sy.
assert (intersectionf sb (fun k => productf two_points(fun i => V (J i k) h))
= intersectionf sb (fun i => product2 (V i f) (V i g))).
app intersectionf_extensionality. ir. uf product2.
app productf_extension. app L_exten1. ir. uf h. try_lvariant H7. aw.
rww Y_if_rw. fprops. aw. rww Y_if_not_rw.
app two_points_distinctb. fprops. wr H6. rw H5.
uf product2. app productf_extension. app L_exten1. ir. uf sb. try_lvariant H7;
uf intersectionb; try wr H1; app intersectionf_extensionality;
ir; uf h; bw; fprops; aw. rww Y_if_rw. rww Y_if_not_rw.
app two_points_distinctb.
Qed.
Product of two products of family of sets
Definition prod_of_function x x':=
L(domain x)(fun i => J (V i x) (V i x')).
Definition prod_of_products_canon f f':=
BL(fun w => prod_of_function (P w) (Q w))
(product (productb f) (productb f'))
(productf (domain f)(fun i => product (V i f) (V i f'))).
Definition prod_of_product_aux f f' :=
fun i => (product (W i f) (W i f')).
Definition prod_of_prod_target f f' :=
fun_image(source f)(prod_of_product_aux f f').
Definition prod_of_products f f' :=
BL (prod_of_product_aux f f')(source f)(prod_of_prod_target f f').
Lemma prod_of_prod_inc_target: forall f f' x,
inc x (prod_of_prod_target f f') =
(exists i, inc i (source f) & product (W i f) (W i f') = x).
Proof. ir. uf prod_of_prod_target. aw.
Qed.
Lemma prod_of_products_function: forall f f',
is_function (prod_of_products f f').
Proof. ir. uf prod_of_products. app bl_function. red. ir.
rw prod_of_prod_inc_target. ex_tac.
Qed.
Lemma prod_of_products_source: forall f f',
source (prod_of_products f f') = source f.
Proof. ir. uf prod_of_products. aw.
Qed.
Lemma prod_of_products_target: forall f f',
target (prod_of_products f f') = prod_of_prod_target f f'.
Proof. ir. uf prod_of_products. aw.
Qed.
Lemma prod_of_products_W: forall f f' i,
inc i (source f) ->
W i (prod_of_products f f') = product (W i f) (W i f').
Proof. ir. uf prod_of_products. aw.
red. ir. rw prod_of_prod_inc_target. ex_tac.
Qed.
Lemma prod_of_products_fam_pr: forall f f' x,
is_function x -> source x = source f ->
target x = union (prod_of_prod_target f f') ->
inc (graph x) (productb (graph (prod_of_products f f'))) =
forall i, inc i (source f) ->
(is_pair (W i x) & inc (P (W i x)) (W i f) & inc (Q (W i x)) (W i f')).
Proof. ir.
assert (Hb:is_function (prod_of_products f f')).
app prod_of_products_function.
assert (Ha:fgraph (graph (prod_of_products f f'))). fprops.
app iff_eq. ir. awi H2.
assert (domain (graph x) = source x). red in H;ee; sy; am.
cp (prod_of_products_W f' H3). ufi W H5. nin H2. nin H6. wri H0 H3.
cp (H7 _ H3). rwi H5 H8. awi H8. uf W. eee. am. am. fprops.
ir. aw. ee. fprops. rww prod_of_products_source.
ir. rwi H0 H3. cp (prod_of_products_W f' H3).
change (inc (W i x) (W i (prod_of_products f f'))). rw H4. set (H2 _ H3). aw.
Qed.
Lemma prod_of_function_axioms:forall x x' f f',
is_function f -> is_function f' -> source f = source f' ->
inc (graph x) (productb (graph f)) -> inc (graph x') (productb (graph f')) ->
transf_axioms (fun i => J (W i x) (W i x'))
(source f) (union (prod_of_prod_target f f')).
Proof. ir.
assert (forall c, inc c (source f) ->
inc (J (W c x) (W c x')) (product (W c f) (W c f'))).
ir. rwi productb_rw H2. rwi productb_rw H3. ee.
assert (inc (W c x) (W c f)). red in H. ee. rwi H10 H4. uf W. app H8. ue.
assert (inc (W c x') (W c f')). red in H0. rwi H1 H4. uf W. ee.
rwi H11 H4. app H6. ue. fprops. fprops. fprops. red. ir.
apply union_inc with (product (W c f) (W c f')).
app H4. rw prod_of_prod_inc_target. ex_tac.
Qed.
Lemma prod_of_function_W:forall x x' f f' i,
is_function f -> is_function f' -> source f = source f' ->
inc x (productb (graph f)) -> inc x' (productb (graph f')) ->
inc i (source f) ->
V i (prod_of_function x x') = J (V i x) (V i x').
Proof. ir. uf prod_of_function. bw.
awi H2. ee. ue. am. fprops.
Qed.
Lemma prod_of_function_function: forall x x' f f',
is_function f -> is_function f' -> source f = source f' ->
inc x (productb (graph f)) -> inc x' (productb (graph f')) ->
inc (prod_of_function x x')
(productb (graph (prod_of_products f f'))).
Proof. ir. assert (Ha:=prod_of_products_function f f').
assert (forall c, inc c (source f) ->
inc (J (V c x) (V c x')) (product (W c f) (W c f'))).
ir. rwi productb_rw H2. rwi productb_rw H3. ee.
assert (inc (V c x) (W c f)). rwi H7 H8. red in H. ee. rwi H10 H4. uf W.
app H8.
assert (inc (V c x') (W c f')). rwi H1 H4. red in H0. ee. rwi H11 H4.
rwi H5 H6. uf W. app H6. fprops. fprops. fprops. aw.
uf prod_of_function. ee. gprops. bw. rw prod_of_products_source. awi H2.
eee. am. fprops. bw. ir. bw. awi H2. ee. rwi H6 H5.
cp (prod_of_products_W f' H5). unfold W in H8. rw H8.
ufi W H4. app H4. am. fprops. fprops.
Qed.
Lemma popc_target_aux:forall f f',
is_function f -> is_function f' -> source f = source f' ->
productb(L (domain (graph f))
(fun i => product (V i (graph f)) (V i (graph f')))) =
productb (graph (prod_of_products f f')).
Proof. ir. app uneq.
assert (is_function (prod_of_products f f')). app prod_of_products_function.
app fgraph_exten. gprops. fprops. bw. aw. uf prod_of_products. aw.
bw. ir. bw. red in H. ee. wri H5 H3. cp (prod_of_products_W f' H3).
sy. ufi W H6. am.
Qed.
Lemma popc_target:forall f f',
is_function f -> is_function f' -> source f = source f' ->
target (prod_of_products_canon (graph f) (graph f')) =
(productb (graph (prod_of_products f f'))).
Proof. ir. uf prod_of_products_canon. simpl. uf productf. rww popc_target_aux.
aw.
Qed.
Lemma popc_axioms:forall f f',
is_function f -> is_function f' -> source f = source f' ->
transf_axioms(fun w => prod_of_function (P w) (Q w))
(product (productb (graph f)) (productb (graph f')))
(productb (graph (prod_of_products f f'))).
Proof. ir. red. ir. rwi product_inc_rw H2. ee. app prod_of_function_function.
Qed.
Lemma popc_W:forall f f' w,
is_function f -> is_function f' -> source f = source f' ->
inc w (product (productb (graph f)) (productb (graph f'))) ->
W w (prod_of_products_canon (graph f) (graph f')) =
prod_of_function (P w) (Q w).
Proof. ir. uf prod_of_products_canon. rw bl_W. tv.
uf productf. rww popc_target_aux. app popc_axioms. am.
Qed.
Lemma popc_bijection:forall f f',
is_function f -> is_function f' -> source f = source f' ->
bijective (prod_of_products_canon (graph f) (graph f')).
Proof. ir. set (g:= prod_of_products_canon (graph f) (graph f')).
assert (Hu: source g = product (productb (graph f)) (productb (graph f'))).
uf g. uf prod_of_products_canon. aw.
assert (is_function g). uf g.
uf prod_of_products_canon. app bl_function.
uf productf. rww popc_target_aux. app popc_axioms.
red. ee. red. ee. am. ir. rwi Hu H3; rwi Hu H4. ufi g H5. rwii popc_W H5.
rwii popc_W H5. rwi product_inc_rw H3. rwi product_inc_rw H4. ee.
assert (forall i, inc i (source f) ->
J (V i (P x)) (V i (Q x)) = J (V i (P y)) (V i (Q y))). ir.
rewrite <- prod_of_function_W with (f:=f)(f':=f'); tv.
rewrite <- prod_of_function_W with (f:=f)(f':=f');tv. ue.
assert (P x = P y). apply productb_exten with (f:=(graph f)). fprops. am. am.
ir. red in H. ee. wri H13 H11. pose (H10 _ H11). inter2tac.
assert (Q x = Q y). apw productb_exten (graph f'). fprops.
ir. red in H0. ee. wri H14 H12. wri H1 H12. pose(H10 _ H12). inter2tac.
app pair_extensionality.
assert (is_function (prod_of_products f f')). app prod_of_products_function.
app surjective_pr6. uf g. rww popc_target. ir. fold g. rw Hu. awi H4. ee.
rwi prod_of_products_source H5.
set (xa:= BL(fun i => P(V i y)) (source f)(union (target f))).
set (xb:= BL(fun i => Q(V i y)) (source f)(union (target f'))).
assert(transf_axioms (fun i => P (V i y)) (source f) (union (target f))).
red. ir. cp (prod_of_products_W f' H7). ufi W H8.
rwi H5 H6. cp (H6 _ H7). rwi H8 H9. awi H9. eee.
apply union_inc with (V c (graph f)). am.
assert (sub (range (graph f)) (target f)). nin H. fprops. app H12.
app inc_V_range. fprops. red in H; ee. wr H14. ue. ue.
assert(transf_axioms (fun i => Q (V i y)) (source f')(union (target f'))).
red. ir. wri H1 H8. cp (prod_of_products_W f' H8). ufi W H9.
wri H5 H8. cp (H6 _ H8). rwi H9 H10. awi H10. eee.
apply union_inc with (V c (graph f')). am.
assert (sub (range (graph f')) (target f')). nin H0. fprops. app H13.
app inc_V_range. fprops. red in H0; ee. wr H15. wr H1. ue.
assert (is_function xa). uf xa. app bl_function.
assert (is_function xb). uf xb. app bl_function. ue.
assert (inc (graph xa) (productb (graph f))). aw.
ee. fprops. fprops. uf xa. aw.
ir. change (inc (W i xa) (W i f)). ufi xa H11. awi H11.
assert (W i xa = P (V i y)). uf xa. aw. rw H12.
cp (prod_of_products_W f' H11). wri H5 H11. cp (H6 _ H11). ufi W H13.
rwi H13 H14. awi H14. eee. fprops.
assert (inc (graph xb) (productb (graph f'))). aw.
ee. fprops. fprops. uf xb. aw.
ir. change (inc (W i xb) (W i f')). ufi xb H12. awi H12.
assert (W i xb = Q (V i y)). uf xb. rw H1. aw. ue. rw H13.
cp (prod_of_products_W f' H12). wri H5 H12. cp (H6 _ H12). ufi W H14.
rwi H14 H15. awi H15. eee. fprops.
exists (J (graph xa) (graph xb)). ee. fprops. uf g. rww popc_W.
aw. uf prod_of_function. sy. ap fgraph_exten. am. gprops.
bw. red in H9. ee. wrr H14. uf xa. aw.
ir. bw.
assert (V x (graph xa) = W x xa). tv. rw H14. uf xa. aw.
assert (V x (graph xb) = W x xb). tv. rw H15. uf xb. aw.
cp (H6 _ H13). rwi H5 H13. cp (prod_of_products_W f' H13). ufi W H17.
rwi H17 H16. awi H16. ee. am. ue. ue. ue. red in H9. ee. wrr H15. uf xa.
aw. ue. fprops. am. fprops.
Qed.
Definition ext_map_prod_aux x f := fun i=> V (V i x) (f i).
Definition ext_map_prod I src trg f :=
BL (fun x => L I (ext_map_prod_aux x f))
(productf I src ) (productf I trg ).
Definition ext_map_prod_axioms I src trg f :=
forall i, inc i I -> (fgraph (f i) & domain (f i) = src i &
sub (range (f i)) (trg i)).
Lemma ext_map_prod_taxioms: forall I src trg f,
ext_map_prod_axioms I src trg f ->
transf_axioms (fun x => L I (ext_map_prod_aux x f))
(productf I src) (productf I trg).
Proof. ir. red. ir. red in H. aw. ee. gprops. bw. bw. ir. bw.
uf ext_map_prod_aux. awi H0. ee. cp (H _ H1). ee. app H6.
app inc_V_range. rw H5. rwi H2 H3. app H3.
Qed.
Lemma ext_map_prod_function: forall I src trg f,
ext_map_prod_axioms I src trg f -> is_function ( ext_map_prod I src trg f).
Proof. ir. uf ext_map_prod. app bl_function. app ext_map_prod_taxioms.
Qed.
Lemma ext_map_prod_W: forall I src trg f x,
ext_map_prod_axioms I src trg f ->
inc x (productf I src) ->
W x (ext_map_prod I src trg f) = L I (ext_map_prod_aux x f).
Proof. ir. uf ext_map_prod. aw. app ext_map_prod_taxioms.
Qed.
Lemma ext_map_prod_WV: forall I src trg f x i,
ext_map_prod_axioms I src trg f ->
inc x (productf I src) -> inc i I ->
V i (W x (ext_map_prod I src trg f)) = V (V i x) (f i).
Proof. ir. rww ext_map_prod_W. bw.
Qed.
Lemma ext_map_prod_composable: forall I p1 p2 p3 g f h,
ext_map_prod_axioms I p1 p2 f ->
ext_map_prod_axioms I p2 p3 g ->
(forall i, inc i I -> h i = fcompose (g i) (f i)) ->
(forall i, inc i I -> fcomposable (g i) (f i)) ->
ext_map_prod_axioms I p1 p3 h.
Proof. ir. ee. red in H; red in H0; red. ir.
cp (H _ H3). cp (H0 _ H3). clear H; clear H0. ee. rw H1.
app fcompose_fgraph. am. rw H1. wr H6. app fcomposable_domain. app H2. am.
rw H1. red. ir. srwi H8. nin H8. ee. rwi fcompose_ev H9.
app H5. rw H9. srw. exists (V x0 (f i)). ee. rw H0.
app H7. srw. exists x0. ee. rwi fcomposable_domain H8. am.
app H2. tv. tv. am. app fcompose_fgraph. am.
Qed.
Lemma ext_map_prod_compose: forall I p1 p2 p3 g f h,
ext_map_prod_axioms I p1 p2 f ->
ext_map_prod_axioms I p2 p3 g ->
(forall i, inc i I -> h i = fcompose (g i) (f i)) ->
(forall i, inc i I -> fcomposable (g i) (f i)) ->
compose (ext_map_prod I p2 p3 g) (ext_map_prod I p1 p2 f) =
(ext_map_prod I p1 p3 h).
Proof. ir.
assert (composable (ext_map_prod I p2 p3 g)
(ext_map_prod I p1 p2 f) ).
red. ee; try app ext_map_prod_function. uf ext_map_prod; aw.
assert (is_function (compose(ext_map_prod I p2 p3 g)
(ext_map_prod I p1 p2 f))). fct_tac.
app function_exten. app ext_map_prod_function.
app (ext_map_prod_composable h H H0 H1 H2).
aw. uf ext_map_prod. aw. uf ext_map_prod. aw.
ir. ufi ext_map_prod H5. rwi compose_source H5. rwi bl_source H5.
set (f1:= (ext_map_prod I p1 p2 f)).
set (t:= W x f1).
assert(t = L I (ext_map_prod_aux x f)). uf t. uf f1. rww ext_map_prod_W.
set (g1:= (ext_map_prod I p2 p3 g)).
assert (W t g1 = L I (ext_map_prod_aux t g)). uf g1. rww ext_map_prod_W.
uf t. assert (target f1 = productf I p2). uf f1. uf ext_map_prod. aw.
wr H7. app inc_W_target. uf f1. app ext_map_prod_function.
uf f1. uf ext_map_prod. rww bl_source.
set (h1:= (ext_map_prod I p1 p3 h)).
assert (W x h1 = L I (ext_map_prod_aux x h)). uf h1. rww ext_map_prod_W.
app (ext_map_prod_composable h H H0 H1 H2). aw. fold t.
rw H7;rw H8. app L_exten1. ir. rw H6. uf ext_map_prod_aux.
bw. set (y:= (V x0 x)). rw H1. rww fcompose_ev.
rw fcomposable_domain. uf y. red in H. ee. cp (H _ H9). ee. rw H11.
awi H5. ee. app H14. ue. app H2. am. uf f1. uf ext_map_prod. rww bl_source.
Qed.
Lemma ext_map_prod_injective: forall I p1 p2 f,
ext_map_prod_axioms I p1 p2 f ->
(forall i, inc i I -> injective_graph (f i)) ->
injective (ext_map_prod I p1 p2 f).
Proof. ir. red. ir. ee. app ext_map_prod_function.
ir. ufi ext_map_prod H1. ufi ext_map_prod H2.
rwi bl_source H1; rwi bl_source H2. ap (productf_exten H1 H2). ir.
cp (ext_map_prod_WV H H1 H4). rwi H3 H5.
cp (ext_map_prod_WV H H2 H4). rwi H5 H6. cp (H0 _ H4). red in H7. ee.
app H8. red in H. cp (H i H4). ee. rw H10. awi H1. ee. app H13.
ue. red in H. cp (H i H4). ee. rw H10. awi H2. ee. app H13. ue.
Qed.
Lemma ext_map_prod_surjective: forall I p1 p2 f,
ext_map_prod_axioms I p1 p2 f ->
(forall i, inc i I -> range (f i) = p2 i) ->
surjective (ext_map_prod I p1 p2 f).
Proof. ir. app surjective_pr6. app ext_map_prod_function. ir.
ufi ext_map_prod H1. rwi bl_target H1. assert (Ha:= H1). awi H1. ee.
rwi H2 H3.
assert (forall i, inc i I -> exists z, inc z (p1 i) & V i y =V z (f i)).
ir. cp (H _ H4). ee. cp (H0 _ H4). cp (H3 _ H4). wri H8 H9. srwi H9. ue. am.
set (x:= L I (fun i => choose (fun z => inc z (p1 i) & V i y = V z (f i)))).
assert (forall i, inc i I -> (inc (V i x) (p1 i) & V i y = V (V i x) (f i))).
ir. uf x. bw. app choose_pr. app H4.
assert (inc x (productf I p1)). aw. ee. uf x. gprops.
uf x. bw. ir. ufi x H6. bwi H6. cp (H5 _ H6). ee. am.
set (q := ext_map_prod I p1 p2 f).
assert (inc x (source q)). uf q. uf ext_map_prod. rww bl_source.
assert (inc (W x q)(productf I p2)).
assert (target q = (productf I p2)). uf q. uf ext_map_prod. aw. wr H8.
app inc_W_target. uf q. app ext_map_prod_function. ex_tac.
ap (productf_exten H8 Ha). ir. uf q. rww ext_map_prod_WV. nin (H5 _ H9).
sy; am.
Qed.
Lemma fun_set_to_prod1: forall F f i,
fgraph F -> inc i (domain F) ->
is_function f -> target f = productb F ->
(is_function (compose (pr_i F i) f) &
source (compose (pr_i F i) f) = source f &
target (compose (pr_i F i) f) = V i F&
(forall x, inc x (source f) -> W x (compose (pr_i F i) f) = V i (W x f))).
Proof. ir. assert (composable (pr_i F i) f). red. ee. app pri_function.
am. uf pr_i; aw. sy; tv. ee. fct_tac. uf pr_i. aw. uf pr_i. aw.
ir. aw. rw pri_W. tv. am. am. wr H2. fprops.
Qed.
The two sets (prod Fi)^E and prod (Fi^E) are isomorphic
Definition fun_set_to_prod src F :=
BL(fun f =>
L(domain F)( fun i=> (graph (compose (pr_i F i)
(corresp src (productb F) f)))))
(set_of_gfunctions src (productb F))
(productb (L (domain F) (fun i=> set_of_gfunctions src (V i F)))).
Lemma fun_set_to_prod2: forall src F f gf,
fgraph F -> inc gf (set_of_gfunctions src (productb F)) ->
f = (corresp src (productb F) gf) ->
(is_function f & target f = productb F & source f = src).
Proof. ir. nin (set_of_gfunctions_inc H0).
assert (x = f). rw H1. ee. wr H3; wr H4;wr H5. sy; app corresp_recov.
nin H2; nin H2. am. wr H3. intuition.
Qed.
Lemma fun_set_to_prod3: forall src F,
fgraph F -> transf_axioms(fun f =>
L(domain F)( fun i=> (graph (compose (pr_i F i)
(corresp src (productb F) f)))))
(set_of_gfunctions src (productb F))
(productb (L (domain F) (fun i=> set_of_gfunctions src (V i F)))).
Proof. ir. red. ir. set (f:=(corresp src (productb F) c)).
cp (fun_set_to_prod2 H H0 (refl_equal f)). ee. aw.
bw. ee. gprops. tv. ir. bw. cp (fun_set_to_prod1 H H4 H1 H2). ee.
wr H3; wr H6; wr H7. app inc_set_of_gfunctions. gprops.
Qed.
Lemma fun_set_to_prod4: forall src F,
fgraph F -> ( is_function (fun_set_to_prod src F)
& source (fun_set_to_prod src F) = (set_of_gfunctions src (productb F))
& target (fun_set_to_prod src F)
= (productb (L (domain F) (fun i=> set_of_gfunctions src (V i F))))).
Proof. ir. uf fun_set_to_prod. ee. app bl_function. app fun_set_to_prod3.
aw. aw.
Qed.
Definition fun_set_to_prod5 F f :=
ext_map_prod (domain F) (fun i=> source f)(fun i=> V i F)
(fun i => (graph (compose (pr_i F i) f))).
Lemma fun_set_to_prod6: forall F f,
fgraph F -> is_function f -> target f = productb F ->
(is_function (fun_set_to_prod5 F f) &
composable (fun_set_to_prod5 F f) (constant_functor (domain F)(source f) )&
compose (fun_set_to_prod5 F f) (constant_functor (domain F)(source f)) =f).
Proof. ir. set (tf := fun_set_to_prod5 F f).
assert (is_function tf). uf tf. uf fun_set_to_prod5.
app ext_map_prod_function. red. ir. cp (fun_set_to_prod1 H H2 H0 H1).
ee. fprops. red in H3. ee. wr H8; rw H4. tv. wr H5. red in H3; ee. fprops.
assert (productb F = target tf). uf tf. uf fun_set_to_prod5.
uf ext_map_prod. aw. uf productf. app uneq. app fgraph_exten.
gprops. bw. ir. bw.
assert(composable tf (constant_functor (domain F)(source f))).
red. ee. am. uf constant_functor. app bl_function. red. ir.
rw graphset_pr2. uf constant_graph. bw. ee. gprops.
tv. red. ir. bwi H5. nin H5. ee. ue.
set (k:= L (domain F) (fun _ : Set => source f)).
assert (domain F = domain k). uf k. bw. rw H4.
uf constant_functor. aw. wrr product_eq_graphset.
uf tf. uf fun_set_to_prod5. uf ext_map_prod. aw. uf k. gprops.
ir. uf k. bw. ue.
eee. sy. app function_exten. fct_tac. uf constant_functor. aw.
uf tf. uf fun_set_to_prod5. uf ext_map_prod. aw.
uf productf. rw H1. rww L_recovers.
ir. uf constant_functor. aw.
assert (inc (W x f) (productb F)). wr H1. fprops.
assert (inc (W (constant_graph (domain F) x) tf) (productb F)). rw H3.
app inc_W_target. uf tf. uf fun_set_to_prod5. uf ext_map_prod. aw.
aw. uf constant_graph. ee. gprops. bw. bw. ir. bw.
ap (productb_exten H H6 H7). ir. uf tf. uf fun_set_to_prod5.
rw ext_map_prod_W. bw. uf ext_map_prod_aux. uf constant_graph. bw.
assert (V x (graph (compose (pr_i F i) f)) = W x (compose (pr_i F i) f)).
tv. rw H9. aw.
rww pri_W. red. ee. app pri_function. am.
sy. uf pr_i. aw. red. ir. cp (fun_set_to_prod1 H H9 H0 H1). ee.
fprops. red in H10; ee. wr H15. ue. red in H10. wr H12.
app corresp_sub_range. ee. am. aw. uf constant_graph. ee.
gprops. bw. bw. ir. bw.
red. ir. uf constant_graph. uf set_of_gfunctions. Ztac. app powerset_inc.
red. ir. ufi L H7. awi H7. nin H7. ee. wr H8. fprops.
ee. gprops. bw.
Qed.
Lemma fun_set_to_prod7: forall src F f g ,
fgraph F ->
(forall i, inc i (domain F) -> inc (f i) (set_of_gfunctions src (V i F))) ->
g = ext_map_prod (domain F) (fun i=> src)(fun i=> V i F) f ->
(forall i, inc i (domain F) ->
f i = graph (compose (pr_i F i) (compose g (constant_functor (domain F) src) ))).
Proof. ir. assert (is_function (constant_functor (domain F) src)).
uf constant_functor. app bl_function. red. ir. rw graphset_pr2.
uf constant_graph. bw. ee. gprops. tv.
red. ir. bwi H4. nin H4. eee.
assert (is_function g). rw H1. app ext_map_prod_function. red. ir.
cp (H0 _ H4). cp (set_of_gfunctions_inc H5). nin H6. eee.
wr H9. rww f_domain_graph. wr H8. wr H9. app corresp_sub_range. fct_tac.
assert (composable g (constant_functor (domain F) src)).
red. eee. rw H1. uf ext_map_prod. uf constant_functor. aw. uf productf.
set (k:= (L (domain F) (fun _ : Set => src))). assert (domain k = domain F).
uf k. bw. wr H5. assert (fgraph k). uf k. gprops.
assert (forall i, inc i(domain k) -> V i k = src). ir. uf k. bw. ue.
app (product_eq_graphset H6 H7).
assert (is_function (compose g (constant_functor (domain F) src))).
fct_tac.
assert (composable (pr_i F i) (compose g (constant_functor (domain F) src))).
red. ee. app pri_function. am. rw H1. uf pr_i. uf ext_map_prod. aw.
uf productf.
rww L_recovers.
assert(is_function (compose (pr_i F i)
(compose g (constant_functor (domain F) src)))).
fct_tac. cp (H0 _ H2). cp (set_of_gfunctions_inc H9).
nin H10. ee.
assert (x = compose (pr_i F i) (compose g (constant_functor (domain F) src))).
app function_exten. uf pr_i. aw. uf constant_functor. aw.
uf pr_i. aw. ir. aw. uf constant_functor. aw. rw pri_W.
rw H1. rw ext_map_prod_W. bw. uf ext_map_prod_aux.
uf W. wr H13. assert (x0 = (V i (constant_graph (domain F) x0))).
rww constant_graph_V. wrr H15. red. ir.
cp (H0 _ H15). cp (set_of_gfunctions_inc H16). nin H17. eee.
wr H20. rww f_domain_graph. wr H19. red in H17. ee. wr H20.
app corresp_sub_range. aw. ee. uf constant_graph.
gprops. uf constant_graph. bw. uf constant_graph. bw. ir.
bw. wrr H11. uf constant_graph. am. am.
assert (target g = (productb F)). rw H1. uf ext_map_prod. aw.
uf productf. rww L_recovers. wr H15.
app inc_W_target. rw H1. uf ext_map_prod. aw.
aw. ee. uf constant_graph. gprops.
uf constant_graph. bw. uf constant_graph. bw. ir. bw. ue.
red. ir. uf constant_graph.
set (k:= BL(fun _ : Set => c)(domain F) src).
assert (is_function k). uf k. app bl_function. red. ir. am.
cp (inc_set_of_gfunctions H16). ufi k H17. awi H17. ufi BL H17. awi H17. am.
ue. uf constant_functor. aw. ue. uf constant_functor. aw. ue.
sy. ue.
Qed.
Lemma fun_set_to_prod8: forall src F,
fgraph F -> bijective (fun_set_to_prod src F).
Proof. ir. cp (fun_set_to_prod4 src H). ee.
red. ee. red. ee. am. rw H1. ir. cp (set_of_gfunctions_inc H3).
cp (set_of_gfunctions_inc H4). nin H6; nin H7. ee. wr H13; wr H10.
assert (x0 = x1). ufi fun_set_to_prod H5.
cp (fun_set_to_prod3 (src:=src) H). awi H5. clear H14.
app function_exten. ue. ue. ir.
assert (inc (W x2 x0) (productb F)). ue.
assert (inc (W x2 x1) (productb F)). rwi H11 H14. wri H8 H14. ue.
ap (productb_exten H H15 H16). ir.
cp (fun_set_to_prod1 H H17 H7 H9). cp (fun_set_to_prod1 H H17 H6 H12).
ee. wrr H25. wrr H22.
assert (compose (pr_i F i) x0 = compose (pr_i F i) x1).
assert (x0 = corresp src (productb F) x).
wr H11; wr H12; wr H13. rww corresp_recov. nin H6; nin H6. am. wri H26 H5.
assert (x1 = corresp src (productb F) y).
wr H8; wr H9; wr H10. rww corresp_recov. nin H7; nin H7; am. wri H27 H5.
cp (f_equal (V i) H5). bwi H28. app function_exten1. ue. am. am.
ue. ue. ue. am. am. am. am. ue.
app surjective_pr6. uf fun_set_to_prod. aw. ir.
awi H3. ee. bwi H4.
set (x:= BL (fun u=> L (domain F) (fun i=> V u (V i y))) src (productb F)).
assert (Ha:source x = src). uf x. aw.
assert (Hb: target x = (productb F)). uf x. aw.
assert (is_function x). uf x. app bl_function. red. ir. aw.
ee. gprops. bw. bw. ir. bw.
rwi H4 H5. cp (H5 _ H7). bwi H8.
nin (set_of_gfunctions_inc H8). ee. wr H11.
assert (V c (V i y) = W c x0). uf W. rww H12. rw H13. wri H10 H6. fprops. am.
assert (inc (graph x) (set_of_gfunctions src (productb F))). wr Ha; wr Hb.
app inc_set_of_gfunctions. ex_tac.
aw. sy. app fgraph_exten.
gprops. bw. ir. bw. cp (H5 _ H8). bwi H9.
assert (x = corresp src (productb F) (graph x)). wr Ha; wr Hb.
sy. app corresp_recov. nin H6; nin H6; am.
cp (set_of_gfunctions_inc H9). nin H11. ee.
assert (x1 = compose (pr_i F x0) x). app function_exten.
fct_tac. app pri_function. ue. uf pr_i. aw. sy; am. uf pr_i. aw. ue.
uf pr_i. aw. ir. aw. rw pri_W. uf x. aw. bw. uf W. ue. ue.
red. ir. aw. ee. gprops. bw. bw. ir.
bw. rwi H4 H5. cp (H5 _ H17). bwi H18.
nin (set_of_gfunctions_inc H18). ee.
wr H22. wr H21. change (inc (W c x3) (target x3)). wri H20 H16. fprops.
am. ue. am. ue. wr Hb. app inc_W_target. rwi H12 H15. ue.
red. ee. app pri_function. ue. am. uf pr_i. aw. sy; am. rwi H12 H15. ue.
wr H10. wr H15. sy; am. ue. ue.
app (fun_set_to_prod3 H (src:=src)). gprops.
Qed.
End Bproduct.
Export Bproduct.