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).

  Lemma Im_add :
    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.