# Library Coq.Sets.Image

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Finite_sets_facts.

Section Image.
Variables U V : Type.

Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y.

Lemma Im_def :
forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).

forall (X:Ensemble U) (x:U) (f:U -> V),
Im (Add _ X x) f = Add _ (Im X f) (f x).

Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.

Lemma finite_image :
forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).

Lemma Im_inv :
forall (X:Ensemble U) (f:U -> V) (y:V),
In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y.

Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.

Lemma not_injective_elim :
forall f:U -> V,
~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y).

Lemma cardinal_Im_intro :
forall (A:Ensemble U) (f:U -> V) (n:nat),
cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p.

Lemma In_Image_elim :
forall (A:Ensemble U) (f:U -> V),
injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.

Lemma injective_preserves_cardinal :
forall (A:Ensemble U) (f:U -> V) (n:nat),
injective f ->
cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.

Lemma cardinal_decreases :
forall (A:Ensemble U) (f:U -> V) (n:nat),
cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.

Theorem Pigeonhole :
forall (A:Ensemble U) (f:U -> V) (n:nat),
cardinal U A n ->
forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.

Lemma Pigeonhole_principle :
forall (A:Ensemble U) (f:U -> V) (n:nat),
cardinal _ A n ->
forall n':nat,
cardinal _ (Im A f) n' ->
n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y).

End Image.

#[global]
Hint Resolve Im_def image_empty finite_image: sets.