Browse the main library: A B C D E F G or go to appendix or return to overview.

# Library b_functions

initial import of the development

Require Export a_sets.

## Relations

Definition relation R A B := R c= product A B.

Definition dom R := replacement R (fun p => pi1 p).
Definition ran R := replacement R (fun p => pi2 p).
Definition field R := bunion (dom R) (ran R).

Definition symmetric R := forall a b, (a,b) <e R -> (b,a) <e R.
Definition asymmetric R := forall a b, (a,b) <e R -> (b,a) /<e R.
Definition antisymmetric R := forall a b, (a,b) <e R -> (b,a) <e R -> a = b.
Definition transitive R := forall a b c, (a,b) <e R -> (b,c) <e R -> (a,c) <e R.
Definition reflexive R A := forall a, a <e A -> (a,a) <e R.
Definition irreflexive R := forall a, (a,a) /<e R.
Definition linear R A := forall a b, a <e A -> b <e A -> (a,b) <e R \/ (b,a) <e R \/ a = b.

Definition equivalence R A :=
relation R A A /\ symmetric R /\ reflexive R A /\ transitive R.

Definition lordering R A :=
relation R A A /\ asymmetric R /\ transitive R /\ linear R A.

Definition least R A x := x <e A /\ forall y, y <e A -> (x,y) <e R \/ y = x.
Definition wfounded R A := forall M, M c= A -> M <> empty -> exists x, least R M x.
Definition wordering R A := lordering R A /\ wfounded R A.
Definition WO A := exists R, wordering R A.

Lemma rel_pair R A B p a b: relation R A B -> p <e R -> a = pi1 p -> b = pi2 p -> p = (a,b).

Lemma rel_pi f A B p: relation f A B -> p <e f -> (pi1 p, pi2 p) <e f.

Lemma rel_pair1 R A B a b: relation R A B -> (a,b) <e R -> a <e A.

Lemma rel_pair2 R A B a b: relation R A B -> (a,b) <e R -> b <e B.

Lemma rel_pi1 R A B p: relation R A B -> p <e R -> pi1 p <e A.

Lemma rel_pi2 R A B p: relation R A B -> p <e R -> pi2 p <e B.

Lemma asym_irref R: asymmetric R -> antisymmetric R /\ irreflexive R.

Lemma irref_asym R: antisymmetric R /\ irreflexive R -> asymmetric R.

Lemma trans_asym R: transitive R /\ irreflexive R -> asymmetric R.

Lemma wo_irr R A: wordering R A -> irreflexive R.

Lemma wordering_empty: wordering empty empty.

## Functions

Definition total f A B := forall x, x <e A -> exists y, y <e B /\ (x,y) <e f.
Definition functional f := forall a b b', (a,b) <e f -> (a,b') <e f -> b' = b.

Definition surjective f A B := forall y, y <e B -> exists x, x <e A /\ (x,y) <e f.
Definition injective f := forall a a' b, (a,b) <e f -> (a',b) <e f -> a = a'.
Definition bijective f A B := surjective f A B /\ injective f.

Definition function f A B := relation f A B /\ total f A B /\ functional f.

Definition surjection f A B := function f A B /\ surjective f A B.
Definition injection f A B := function f A B /\ injective f.
Definition bijection f A B := function f A B /\ surjective f A B /\ injective f.
Definition equi A B := exists f, bijection f A B.

Lemma fun_pi f A B p: function f A B -> p <e f -> (pi1 p, pi2 p) <e f.

Lemma fun_pair f A B p: function f A B -> p <e f -> p = (pi1 p, pi2 p).

Lemma fun_product f A B p: function f A B -> p <e f -> p <e product A B.

Lemma fun_pi1 f A B p: function f A B -> p <e f -> pi1 p <e A.

Lemma fun_pi2 f A B p: function f A B -> p <e f -> pi2 p <e B.

Lemma fun_pair1 f A B a b: function f A B -> (a,b) <e f -> a <e A.

Lemma fun_pair2 f A B a b: function f A B -> (a,b) <e f -> b <e B.

Lemma fun_el1 f A B a b: function f A B -> (a,b) <e f -> a <e A.

Lemma fun_el2 f A B a b: function f A B -> (a,b) <e f -> b <e B.

Lemma fun_el_dom f a b: (a,b) <e f -> a <e dom f.

Lemma fun_el_ran f a b: (a,b) <e f -> b <e ran f.

Lemma sur_ran1 f A B: relation f A B -> surjective f A B -> ran f = B.

Lemma sur_ran2 f A B: relation f A B -> ran f = B -> surjective f A B.

Lemma sur_ran f A B: relation f A B -> (surjective f A B <-> ran f = B).

Lemma fun_ran_subs f A B: function f A B -> ran f c= B.

Lemma tot_dom1 f A B: relation f A B -> total f A B -> dom f = A.

Lemma tot_dom2 f A B: relation f A B -> dom f = A -> total f A B.

Lemma tot_dom f A B: relation f A B -> (total f A B <-> dom f = A).

Lemma bijec_empty f A: bijection f A empty -> A = empty.

Lemma fun_step_rel f A B x y: function f A B -> x /<e A -> y <e B ->
relation (bunion f (singleton (x,y))) (bunion A (singleton x)) B.

Lemma fun_step_tot f A B x y: function f A B -> x /<e A -> y <e B ->
total (bunion f (singleton (x,y))) (bunion A (singleton x)) B.

Lemma fun_step_fun f A B x y: function f A B -> x /<e A -> y <e B ->
functional (bunion f (singleton (x,y))).

Lemma fun_step f A B x y: function f A B -> x /<e A -> y <e B ->
function (bunion f (singleton (x,y))) (bunion A (singleton x)) B.

Lemma fun_expand f A B B': function f A B -> B c= B' -> function f A B'.

## Application

Definition xgraph f x := specification f (fun p => pi1 p = x).
Definition ximages f x := replacement (xgraph f x) (fun p => pi2 p).
Definition app f x := union (ximages f x).
Notation "f '[' x ']'" := (app f x) (at level 10).

Lemma xgraph_cor f x y: (x,y) <e f -> (x,y) <e xgraph f x.

Lemma im_cor f x y A B: function f A B -> (x,y) <e f -> ximages f x = singleton y.

Lemma app_cor f x A B: function f A B -> x <e A -> (x,f[x]) <e f /\ f[x] <e B.

Lemma app_cor1 f x A B: function f A B -> x <e A -> (x,f[x]) <e f.

Lemma app_cor2 f x A B: function f A B -> x <e A -> f[x] <e B.

Lemma app_eq f x y A B: function f A B -> (x,y) <e f -> y = f[x].

Lemma app_sur f A B y: surjection f A B -> y <e B -> exists x, x <e A /\ y = f[x].

Lemma app_inj f A B x x': injection f A B -> x <e A -> x' <e A -> f[x] = f[x'] -> x = x'.

Lemma fun_app f A B p: function f A B -> p <e f -> pi2 p = f[pi1 p].

Lemma fun_appel f A B p: function f A B -> p <e f -> p = (pi1 p, f[pi1 p]).

Lemma bij_app f A B p: bijection f A B -> p <e f -> pi2 p = f[pi1 p].

Lemma fun_shrink A B B' f: function f A B -> (forall x, x <e A -> f[x] <e B') -> function f A B'.

## Restriction

Definition restriction f A := specification f (fun p => pi1 p <e A).
Notation "f | A" := (restriction f A) (at level 8).

Definition rel_restriction R A := specification R (fun p => p <e product A A).
Notation "R '|>' A" := (rel_restriction R A) (at level 9).

Lemma res_functional f A: functional f -> functional f|A.

Lemma res_injective f A: injective f -> injective f|A.

Lemma res_fun f A B A': function f A B -> A' c= A -> function (f|A') A' B.

Lemma res_el f A B A' x y: function f A B -> A' c= A -> (x,y) <e f | A' -> x <e A'.

Lemma res_eq f A B A' x: function f A B -> A' c= A -> x <e A' -> f [x] = f|A' [x].

Lemma res_opair f A B A' a b: function f A B -> A' c= A -> (a,b) <e f -> a <e A' -> (a,b) <e f|A'.

Lemma res_res f A B: A c= B -> (f|B)|A = f|A.

Lemma relres_rel R A': relation (R|>A') A' A'.

Lemma relres_asym R A': asymmetric R -> asymmetric (R|>A').

Lemma relres_trans R A': transitive R -> transitive (R|>A').

Lemma relres_linear R A A': linear R A -> A' c= A -> linear (R|>A') A'.

Lemma relres_wf R A A': wfounded R A -> A' c= A -> wfounded (R|>A') A'.

Lemma worder_subs R A A': wordering R A -> A' c= A -> wordering (R|>A') A'.

Lemma equi_empty A B: equi A B -> A <> empty -> B <> empty.

## Image

Definition image f A := replacement f|A (fun p => pi2 p).
Notation "f '[(' A ')]'" := (image f A) (at level 10).

Lemma image_subs f A B A': function f A B -> image f A' c= B.

Lemma image_empty f A B A': function f A B -> A' c= A -> A' <> empty -> image f A' <> empty.

Lemma im_el f A B A' x y: injection f A B -> A' c= A -> (x,y) <e f -> y <e image f A' -> x <e A'.

Lemma image_el f A B A' x: function f A B -> A' c= A -> x <e A' -> f[x] <e image f A'.

Lemma image_res f A B A': function f A B -> A' c= A -> f|A'[(A')] = f[(A')].

Lemma image_rel f A B A': bijection f A B -> A' c= A -> relation (f|A') A' (f[(A')]).

Lemma image_tot f A B A': bijection f A B -> A' c= A -> total (f|A') A' (f[(A')]).

Lemma image_sur f A B A': bijection f A B -> A' c= A -> surjective (f|A') A' (f[(A')]).

Lemma image_bijection f A B A': bijection f A B -> A' c= A -> bijection (f|A') A' (f[(A')]).

Lemma image_bij f A B A': bijection f A B -> A' c= A -> bijection (f|A') A' (f|A'[(A')]).

Lemma fun_ran f A B: function f A B -> function f A (ran f).

Lemma image_ran f A B A': A' c= A -> function f A B -> image f A' = ran (f|A').

Lemma equi_subs A B A': equi A B -> A' c= A -> exists B', B' c= B /\ equi A' B'.

## Inverse

Definition inverse f := replacement f (fun p => (pi2 p, pi1 p)).
Notation "f ^" := (inverse f) (at level 5).

Lemma inv_el1 f x y: (x,y) <e f -> (y,x) <e f^.

Lemma inv_el2 f x y A B: relation f A B -> (y,x) <e f^ -> (x,y) <e f.

Lemma inv_bij f A B: bijection f A B -> bijection f^ B A.

Lemma inv_el f A B y: bijection f A B -> y <e B -> f^[y] <e A.

Lemma inv_element f A B y: bijection f A B -> y <e B -> (f^[y], y) <e f.

Lemma inv_idem f A B: bijection f A B -> f = f^^.

Lemma inv1 f A B x: bijection f A B -> x <e A -> x = f^[f[x]].

Lemma inv2 f A B y: bijection f A B -> y <e B -> y = f[f^[y]].

Lemma equi_com A B: equi A B -> equi B A.

## Composition

Definition comp f g :=
specification (product (dom g) (ran f)) (fun p => exists b, (pi1 p, b) <e g /\ (b, pi2 p) <e f).

Lemma comp_rel f g A B C: function f B C -> function g A B -> relation (comp f g) A C.

Lemma comp_tot f g A B C: function f B C -> function g A B -> total (comp f g) A C.

Lemma comp_fct f g A B C: function f B C -> function g A B -> functional (comp f g).

Lemma comp_fun f g A B C: function f B C -> function g A B -> function (comp f g) A C.

Lemma comp_app A B C f g x: bijection f B C -> bijection g A B -> x <e A -> (comp f g)[x] = f[g[x]].

Lemma comp_sur f g A B C: bijection f B C -> bijection g A B -> surjective (comp f g) A C.

Lemma comp_inj f g A B C: bijection f B C -> bijection g A B -> injective (comp f g).

Lemma comp_bij f g A B C: bijection f B C -> bijection g A B -> bijection (comp f g) A C.

Lemma equi_trans A B C: equi A B -> equi B C -> equi A C.

## The Identity Function

Definition id A := specification (product A A) (fun p => pi1 p = pi2 p).

Lemma id_bijection A: bijection (id A) A A.

Lemma id_app A a: a <e A -> (id A)[a] = a.

Lemma id_equal A B: bijection (id A) A B -> A = B.

Lemma id_rel f A B: function f A B -> (forall x, x <e A -> (x,x) <e f) -> relation f A A.

Lemma id_fun f A B: function f A B -> (forall x, x <e A -> (x,x) <e f) -> id A = f.

## Functions are Extensional

Lemma fun_subs1 A B f g: function f A B -> function g A B ->
(forall b, b <e A -> f[b] = g[b]) -> f c= g.

Lemma fun_subs2 A B f g: function f A B -> function g A B ->
(forall b, b <e A -> f[b] = g[b]) -> g c= f.

Lemma fun_eq A B f g: function f A B -> function g A B ->
(forall b, b <e A -> f[b] = g[b]) -> f = g.

Lemma fun_eq_gen A B B' f g: function f A B -> function g A B' ->
(forall x, x <e A -> f[x] = g[x]) -> f = g.

Lemma fun_res_eq A B B' f g A': function f A B -> function g A B' -> A' c= A ->
(forall b, b <e A' -> f[b] = g[b]) -> f|A' = g|A'.

Lemma fun_subs f g A B A' x: function f A B -> function g A' B -> x <e A'
-> g c= f -> g [x] = f [x].

Lemma fun_subs_res f g A B A' C: function f A B -> function g A' B
-> g c= f -> C c= A' -> A' c= A -> f|C = g|C.

## Meta-Functions and Object-Functions

Definition lam f A := replacement A (fun a => (a,f a)).
Definition sur f A B := forall y, y <e B -> exists x, x <e A /\ f x = y.
Definition inj f A:= forall x x' (y:set), x <e A -> x' <e A -> f x = y -> f x' = y -> x = x'.

Lemma lam_el f A x y: (x,y) <e (lam f A) -> f x = y /\ x <e A.

Lemma lam_fun f A B: (forall x, x <e A -> f x <e B) -> function (lam f A) A B.

Lemma lam_app F A B x: (forall x, x <e A -> F x <e B) -> x <e A -> F x = (lam F A) [x].

Lemma lam_app2 F A B x: function (lam F A) A B -> x <e A -> F x = (lam F A) [x].

Lemma lam_subs F A A': A' c= A -> (lam F A) | A' = lam F A'.

Lemma lam_sur F A B: sur F A B -> surjective (lam F A) A B.

Lemma lam_inj F A: inj F A -> injective (lam F A).