Library bijection
- Dimitri Hendriks 2013-10-09
- http://www.cs.vu.nl/~diem/coq/calkin-wilf/bijection.html
Section bijections.
Variables A B : Set.
Definition injective (f : A → B) := ∀ x y : A, f x = f y → x = y.
Definition surjective (f : A → B) := ∀ y : B, {x : A | f x = y}.
Inductive bijective (f : A → B) : Set :=
is_bijective : injective f → surjective f → bijective f.
Definition left_inverse (f : A → B) (f' : B → A) :=
∀ x : A, f' (f x) = x.
Definition right_inverse (f : A → B) (f' : B → A) :=
∀ 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.
Lemma right_inv_surj f f' : right_inverse f f' → surjective f.
Lemma inv2bij f f' : inverse f f' → bijective f.
End bijections.