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.