# Library ZornsLemma.FunctionProperties

Definition injective {X Y:Type} (f:XY) :=
x1 x2:X, f x1 = f x2 x1 = x2.
Definition surjective {X Y:Type} (f:XY) :=
y:Y, x:X, f x = y.
Definition bijective {X Y:Type} (f:XY) :=
injective f surjective f.

Inductive invertible {X Y:Type} (f:XY) : Prop :=
| intro_invertible: g:YX,
( x:X, g (f x) = x) ( y:Y, f (g y) = y)
invertible f.

Require Import Description.
Require Import FunctionalExtensionality.

Lemma unique_inverse: {X Y:Type} (f:XY), invertible f
! g:YX, ( x:X, g (f x) = x)
( y:Y, f (g y) = y).
Proof.
intros.
destruct H.
g.
red; split.
tauto.
intros.
destruct H1.
extensionality y.
transitivity (g (f (x' y))).
rewrite H2.
reflexivity.
rewrite H.
reflexivity.
Qed.

Definition function_inverse {X Y:Type} (f:XY)
(i:invertible f) : { g:YX | ( x:X, g (f x) = x)
( y:Y, f (g y) = y) }
:=
(constructive_definite_description _
(unique_inverse f i)).

Lemma bijective_impl_invertible: {X Y:Type} (f:XY),
bijective f invertible f.
Proof.
intros.
destruct H.
assert ( y:Y, {x:X | f x = y}).
intro.
apply constructive_definite_description.
pose proof (H0 y).
destruct H1.
x.
red; split.
assumption.
intros.
apply H.
transitivity y.
auto with ×.
auto with ×.
pose (g := fun y:Yproj1_sig (X0 y)).
pose proof (fun y:Yproj2_sig (X0 y)).
simpl in H1.
g.
intro.
apply H.
unfold g; rewrite H1.
reflexivity.
intro.
unfold g; apply H1.
Qed.

Lemma invertible_impl_bijective: {X Y:Type} (f:XY),
invertible f bijective f.
Proof.
intros.
destruct H.
split.
red; intros.
congruence.
red; intro.
(g y).
apply H0.
Qed.