Library Stdlib.Lists.Finite
Functions on finite domains
General definitions
Definition Injective {A B} (f : A->B) :=
forall x y, f x = f y -> x = y.
Definition Surjective {A B} (f : A->B) :=
forall y, exists x, f x = y.
Definition Bijective {A B} (f : A->B) :=
exists g:B->A, (forall x, g (f x) = x) /\ (forall y, f (g y) = y).
Finiteness is defined here via exhaustive list enumeration
Definition Full {A:Type} (l:list A) := forall a:A, In a l.
Definition Finite (A:Type) := exists (l:list A), Full l.
In many of the following proofs, it will be convenient to have
list enumerations without duplicates. As soon as we have
decidability of equality (in Prop), this is equivalent
to the previous notion (s. lemma Finite_dec).
Definition Listing {A:Type} (l:list A) := NoDup l /\ Full l.
Definition Finite' (A:Type) := exists (l:list A), Listing l.
Lemma Listing_decidable_eq {A:Type} (l:list A): Listing l -> decidable_eq A.
Lemma Finite_dec {A:Type}: Finite A /\ decidable_eq A <-> Finite' A.
Lemma Finite_alt_deprecated A (d:decidable_eq A) : Finite A <-> Finite' A.
#[deprecated(since="8.17", note="Use Finite_dec instead.")]
Notation Finite_alt := Finite_alt_deprecated.
Injections characterized in term of lists
Lemma Injective_map_NoDup A B (f:A->B) (l:list A) :
Injective f -> NoDup l -> NoDup (map f l).
Lemma Injective_map_NoDup_in A B (f:A->B) (l:list A) :
(forall x y, In x l -> In y l -> f x = f y -> x = y) -> NoDup l -> NoDup (map f l).
Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) :
Injective f <-> (forall l, NoDup l -> NoDup (map f l)).
Lemma Injective_carac A B (l:list A) : Listing l ->
forall (f:A->B), Injective f <-> NoDup (map f l).
Surjection characterized in term of lists
Lemma Surjective_list_carac A B (f:A->B):
Surjective f <-> (forall lB, exists lA, incl lB (map f lA)).
Lemma Surjective_carac A B : Finite B -> decidable_eq B ->
forall f:A->B, Surjective f <-> (exists lA, Listing (map f lA)).
Main result :
Lemma Endo_Injective_Surjective :
forall A, Finite A -> decidable_eq A ->
forall f:A->A, Injective f <-> Surjective f.
An injective and surjective function is bijective.
We need here stronger hypothesis : decidability of equality in Type.
First, we show that a surjective f has an inverse function g such that
f.g = id.
Lemma Finite_Empty_or_not A :
Finite A -> (A->False) \/ exists a:A,True.
Lemma Surjective_inverse :
forall A B, Finite A -> EqDec B ->
forall f:A->B, Surjective f ->
exists g:B->A, forall x, f (g x) = x.
Same, with more knowledge on the inverse function: g.f = f.g = id