Library SCHROEDER.Functions

Require Import Ensembles.
Require Import Relations_1.
Section Functions.

Variable U : Type.

Inductive Rel (U : Type) (A B : Ensemble U) (R : Relation U) : Prop :=
    Rel_intro :
      (forall x y : U, R x y -> In U A x) ->
      (forall x y : U, R x y -> In U B y) -> Rel U A B R.

Section Image.

Inductive Im (R : Relation U) (A : Ensemble U) (y : U) : Prop :=
    Im_intro : forall x : U, R x y -> In U A x -> Im R A y.

Lemma Im_stable_par_incl :
 forall (R : Relation U) (A1 A2 : Ensemble U),
 Included U A1 A2 -> Included U (Im R A1) (Im R A2).
do 3 intro; intros A1_Included_A2; red in |- *; red in |- *;
 intros x x_in_Im_A1.
elim x_in_Im_A1.
intros.
apply Im_intro with x0; try assumption.
apply A1_Included_A2; assumption.
Qed.

End Image.

Variable A B : Ensemble U.
Variable f : Relation U.

Definition au_plus_une_im := forall x y z : U, f x y -> f x z -> y = z.

Definition au_moins_une_im := forall x : U, In U A x -> ex (f x).

Definition au_plus_un_ant := forall x y z : U, f x z -> f y z -> x = y.

Definition au_moins_un_ant := forall y : U, In U B y -> exists x : U, f x y.

Inductive fonction : Prop :=     fonction_intro :
      Rel U A B f -> au_plus_une_im -> au_moins_une_im -> fonction.

Inductive surjection : Prop :=     surjection_intro :
      Rel U A B f ->
      au_plus_une_im -> au_moins_une_im -> au_moins_un_ant -> surjection.

Inductive injection : Prop :=     injection_intro :
      Rel U A B f ->
      au_plus_une_im -> au_moins_une_im -> au_plus_un_ant -> injection.

Inductive bijection : Prop :=     bijection_intro :
      Rel U A B f ->
      au_plus_une_im ->
      au_moins_une_im -> au_plus_un_ant -> au_moins_un_ant -> bijection.

End Functions.