Library ZFrelations
Require Import ZFpairs.
Import IZF.
Definition is_relation x :=
forall p, p \in x -> p == couple (fst p) (snd p).
Definition rel_app r x y := couple x y \in r.
Instance rel_app_morph :
Proper (eq_set ==> eq_set ==> eq_set ==> iff) rel_app.
Qed.
Definition rel_domain r :=
subset (union (union r)) (fun x => exists y, rel_app r x y).
Definition rel_image r :=
subset (union (union r)) (fun y => exists x, rel_app r x y).
Instance rel_image_morph : morph1 rel_image.
Qed.
Lemma rel_image_ex : forall r x, x \in rel_domain r -> exists y, rel_app r x y.
Lemma rel_domain_intro : forall r x y, rel_app r x y -> x \in rel_domain r.
Lemma rel_image_intro : forall r x y, rel_app r x y -> y \in rel_image r.
Definition rel_comp f g :=
subset (prodcart (rel_domain g) (rel_image f))
(fun p => exists2 y, rel_app g (fst p) y & rel_app f y (snd p)).
Lemma rel_comp_intro : forall f g x y z,
rel_app g x y -> rel_app f y z -> rel_app (rel_comp f g) x z.
Definition rel A B := power (prodcart A B).
Lemma rel_mono :
Proper (incl_set ==> incl_set ==> incl_set) rel.
Instance rel_morph : morph2 rel.
Lemma app_typ1 : forall r x y A B, r \in rel A B -> rel_app r x y -> x \in A.
Lemma app_typ2 : forall r x y A B, r \in rel A B -> rel_app r x y -> y \in B.
Lemma rel_is_relation : forall f A B, f \in rel A B -> is_relation f.
Lemma rel_domain_incl : forall r A B, r \in rel A B -> rel_domain r \incl A.
Lemma rel_image_incl : forall r A B, r \in rel A B -> rel_image r \incl B.
Lemma relation_is_rel :
forall r A B,
is_relation r ->
rel_domain r \incl A ->
rel_image r \incl B ->
r \in rel A B.
Definition inject_rel R A B :=
subset (prodcart A B) (fun p => R (fst p) (snd p)).
Lemma inject_rel_is_rel : forall (R:set->set->Prop) A B,
inject_rel R A B \in rel A B.
Lemma inject_rel_intro :
forall (R:set->set->Prop) A B x y,
ext_rel A R ->
x \in A ->
y \in B ->
R x y ->
rel_app (inject_rel R A B) x y.
Lemma inject_rel_elim :
forall (R:set->set->Prop) A B x y,
ext_rel A R ->
rel_app (inject_rel R A B) x y ->
x \in A /\ y \in B /\ R x y.
Definition is_function f :=
is_relation f /\
forall x y y', rel_app f x y -> rel_app f x y' -> y == y'.
Definition app f x :=
union (subset (rel_image f) (fun y => rel_app f x y)).
Instance app_morph : morph2 app.
Lemma app_defined : forall f x y,
is_function f -> rel_app f x y -> app f x == y.
Lemma app_elim : forall f x,
is_function f -> x \in rel_domain f -> rel_app f x (app f x).
Definition func A B :=
subset (rel A B)
(fun r =>
(forall x, x \in A -> exists2 y, y \in B & rel_app r x y) /\
(forall x y y', rel_app r x y -> rel_app r x y' -> y == y')).
Instance func_mono :
Proper (eq_set ==> incl_set ==> incl_set) func.
Qed.
Instance func_morph : morph2 func.
Lemma func_rel_incl : forall A B, func A B \incl rel A B.
Lemma func_is_function : forall f A B, f \in func A B -> is_function f.
Lemma fun_domain_func : forall f A B, f \in func A B -> rel_domain f == A.
Lemma app_typ :
forall f x A B, f \in func A B -> x \in A -> app f x \in B.
Lemma func_narrow : forall f A B B',
f \in func A B ->
(forall x, x \in A -> app f x \in B') ->
f \in func A B'.
Definition lam_rel (F:set->set) A B := inject_rel (fun x y => F x == y) A B.
Lemma lam_rel_is_func : forall A B f,
ext_fun A f ->
(forall x, x \in A -> f x \in B) ->
lam_rel f A B \in func A B.
Lemma beta_rel_eq : forall f x A B,
ext_fun A f ->
x \in A -> (forall x, x \in A -> f x \in B) -> app (lam_rel f A B) x == f x.
Definition lam A F := replf A (fun x => couple x (F x)).
Lemma fun_elt_is_ext : forall A f,
ext_fun A f ->
ext_fun A (fun x => couple x (f x)).
Hint Resolve fun_elt_is_ext.
Lemma lam_is_function : forall A f, ext_fun A f -> is_function (lam A f).
Lemma lam_is_func : forall A B f,
ext_fun A f ->
(forall x, x \in A -> f x \in B) ->
lam A f \in func A B.
Lemma beta_eq : forall f x A,
ext_fun A f -> x \in A -> app (lam A f) x == f x.
Definition dep_image (A:set) (B:set->set) := replf A B.
Lemma dep_image_ext :
forall x1 x2 f1 f2,
x1 == x2 ->
eq_fun x1 f1 f2 ->
dep_image x1 f1 == dep_image x2 f2.
Definition dep_func (A:set) (B:set->set) :=
subset (func A (union (dep_image A B)))
(fun f => forall x, x \in A -> app f x \in B x).
Lemma dep_func_ext :
forall x1 x2 f1 f2,
x1 == x2 ->
eq_fun x1 f1 f2 ->
dep_func x1 f1 == dep_func x2 f2.
Lemma dep_func_intro : forall f dom F,
ext_fun dom f ->
ext_fun dom F ->
(forall x, x \in dom -> f x \in F x) ->
lam dom f \in dep_func dom F.
Lemma func_eta : forall f A B,
f \in func A B ->
f == lam A (fun x => app f x).
Lemma dep_func_eta : forall f dom F,
f \in dep_func dom F ->
f == lam dom (fun x => app f x).
Lemma dep_func_incl_func : forall A B,
dep_func A B \incl func A (union (dep_image A B)).
Lemma dep_func_elim :
forall f x A B, f \in dep_func A B -> x \in A -> app f x \in B x.