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).