bijection
- Dimitri Hendriks 2013-10-09
- http://www.cs.vu.nl/~diem/coq/calkin-wilf/bijection.html
Set Implicit Arguments.
Section bijections.
Variables A B : Type.
Definition injective (f : A -> B) := forall x y : A, f x = f y -> x = y.
Definition surjective (f : A -> B) := forall y : B, {x : A | f x = y}.
Inductive bijective (f : A -> B) : Type :=
is_bijective : injective f -> surjective f -> bijective f.
Definition left_inverse (f : A -> B) (f' : B -> A) :=
forall x : A, f' (f x) = x.
Definition right_inverse (f : A -> B) (f' : B -> A) :=
forall y : B, f (f' y) = y.
Definition inverse f f' :=
left_inverse f f' /\ right_inverse f f'.
Lemma left_inv_inj f f' : left_inverse f f' -> injective f.
Proof.
intros H x y H0.
rewrite <- (H x).
rewrite H0.
apply H.
Qed.
Lemma right_inv_surj f f' : right_inverse f f' -> surjective f.
Proof.
intros H y.
rewrite <- (H y).
exact (exist (fun x => f x = f (f' y)) (f' y) (refl_equal (f (f' y)))).
Qed.
Lemma inv2bij f f' : inverse f f' -> bijective f.
Proof.
intros [H1 H2].
exact (is_bijective (left_inv_inj H1) (right_inv_surj H2)).
Qed.
End bijections.