Image.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

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 Gt.
Require Export Lt.
Require Export Le.
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).U, V:Type
forall (X : Ensemble U) (f : U -> V) (x : U),
In U X x -> In V (Im X f) (f x)
  Proof.U, V:Type
forall (X : Ensemble U) (f : U -> V) (x : U),
In U X x -> In V (Im X f) (f x)
    intros X f x H'; try assumption.U, V:Type
X:Ensemble U
f:U -> V
x:U
H':In U X x
In V (Im X f) (f x)
    apply Im_intro with (x := x); auto with sets.
  Qed.

  Lemma Im_add :
    forall (X:Ensemble U) (x:U) (f:U -> V),
      Im (Add _ X x) f = Add _ (Im X f) (f x).U, V:Type
forall (X : Ensemble U) (x : U) (f : U -> V),
Im (Add U X x) f = Add V (Im X f) (f x)
  Proof.U, V:Type
forall (X : Ensemble U) (x : U) (f : U -> V),
Im (Add U X x) f = Add V (Im X f) (f x)
    intros X x f.U, V:Type
X:Ensemble U
x:U
f:U -> V
Im (Add U X x) f = Add V (Im X f) (f x)
    apply Extensionality_Ensembles.U, V:Type
X:Ensemble U
x:U
f:U -> V
Same_set V (Im (Add U X x) f) (Add V (Im X f) (f x))
    split; red; intros x0 H'.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Im (Add U X x) f) x0
In V (Add V (Im X f) (f x)) x0
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Im (Add U X x) f) x0
    elim H'; intros.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Im (Add U X x) f) x0
x1:U
H:In U (Add U X x) x1
y:V
H0:y = f x1
In V (Add V (Im X f) (f x)) y
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Im (Add U X x) f) x0
    rewrite H0.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Im (Add U X x) f) x0
x1:U
H:In U (Add U X x) x1
y:V
H0:y = f x1
In V (Add V (Im X f) (f x)) (f x1)
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Im (Add U X x) f) x0
    elim Add_inv with U X x x1; auto using Im_def with sets.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Im (Add U X x) f) x0
x1:U
H:In U (Add U X x) x1
y:V
H0:y = f x1
x = x1 -> In V (Add V (Im X f) (f x)) (f x1)
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Im (Add U X x) f) x0
    destruct 1; auto using Im_def with sets.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Im (Add U X x) f) x0
    elim Add_inv with V (Im X f) (f x) x0.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Im X f) x0 -> In V (Im (Add U X x) f) x0
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
f x = x0 -> In V (Im (Add U X x) f) x0
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Add V (Im X f) (f x)) x0
    destruct 1 as [x0 H y H0].U, V:Type
X:Ensemble U
x:U
f:U -> V
y:V
H':In V (Add V (Im X f) (f x)) y
x0:U
H:In U X x0
H0:y = f x0
In V (Im (Add U X x) f) y
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
f x = x0 -> In V (Im (Add U X x) f) x0
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Add V (Im X f) (f x)) x0
    rewrite H0; auto using Im_def with sets.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
f x = x0 -> In V (Im (Add U X x) f) x0
U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Add V (Im X f) (f x)) x0
    destruct 1; auto using Im_def with sets.U, V:Type
X:Ensemble U
x:U
f:U -> V
x0:V
H':In V (Add V (Im X f) (f x)) x0
In V (Add V (Im X f) (f x)) x0
    trivial.
  Qed.

  Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.U, V:Type
forall f : U -> V, Im (Empty_set U) f = Empty_set V
  Proof.U, V:Type
forall f : U -> V, Im (Empty_set U) f = Empty_set V
    intro f; try assumption.U, V:Type
f:U -> V
Im (Empty_set U) f = Empty_set V
    apply Extensionality_Ensembles.U, V:Type
f:U -> V
Same_set V (Im (Empty_set U) f) (Empty_set V)
    split; auto with sets.U, V:Type
f:U -> V
Included V (Im (Empty_set U) f) (Empty_set V)
    red.U, V:Type
f:U -> V
forall x : V,
In V (Im (Empty_set U) f) x -> In V (Empty_set V) x
    intros x H'; elim H'.U, V:Type
f:U -> V
x:V
H':In V (Im (Empty_set U) f) x
forall x0 : U,
In U (Empty_set U) x0 ->
forall y : V, y = f x0 -> In V (Empty_set V) y
    intros x0 H'0; elim H'0; auto with sets.
  Qed.

  Lemma finite_image :
    forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).U, V:Type
forall (X : Ensemble U) (f : U -> V),
Finite U X -> Finite V (Im X f)
  Proof.U, V:Type
forall (X : Ensemble U) (f : U -> V),
Finite U X -> Finite V (Im X f)
    intros X f H'; elim H'.U, V:Type
X:Ensemble U
f:U -> V
H':Finite U X
Finite V (Im (Empty_set U) f)
U, V:Type
X:Ensemble U
f:U -> V
H':Finite U X
forall A : Ensemble U,
Finite U A ->
Finite V (Im A f) ->
forall x : U,
~ In U A x -> Finite V (Im (Add U A x) f)
    rewrite (image_empty f); auto with sets.U, V:Type
X:Ensemble U
f:U -> V
H':Finite U X
forall A : Ensemble U,
Finite U A ->
Finite V (Im A f) ->
forall x : U,
~ In U A x -> Finite V (Im (Add U A x) f)
    intros A H'0 H'1 x H'2; clear H' X.U, V:Type
f:U -> V
A:Ensemble U
H'0:Finite U A
H'1:Finite V (Im A f)
x:U
H'2:~ In U A x
Finite V (Im (Add U A x) f)
    rewrite (Im_add A x f); auto with sets.U, V:Type
f:U -> V
A:Ensemble U
H'0:Finite U A
H'1:Finite V (Im A f)
x:U
H'2:~ In U A x
Finite V (Add V (Im A f) (f x))
    apply Add_preserves_Finite; auto with sets.
  Qed.

  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.U, V:Type
forall (X : Ensemble U) (f : U -> V) (y : V),
In V (Im X f) y -> exists x : U, In U X x /\ f x = y
  Proof.U, V:Type
forall (X : Ensemble U) (f : U -> V) (y : V),
In V (Im X f) y -> exists x : U, In U X x /\ f x = y
    intros X f y H'; elim H'.U, V:Type
X:Ensemble U
f:U -> V
y:V
H':In V (Im X f) y
forall x : U,
In U X x ->
forall y0 : V,
y0 = f x -> exists x0 : U, In U X x0 /\ f x0 = y0
    intros x H'0 y0 H'1; rewrite H'1.U, V:Type
X:Ensemble U
f:U -> V
y:V
H':In V (Im X f) y
x:U
H'0:In U X x
y0:V
H'1:y0 = f x
exists x0 : U, In U X x0 /\ f x0 = f x
    exists x; auto with sets.
  Qed.

  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).U, V:Type
forall f : U -> V,
~ injective f -> exists x y : U, f x = f y /\ x <> y
  Proof.U, V:Type
forall f : U -> V,
~ injective f -> exists x y : U, f x = f y /\ x <> y
    unfold injective; intros f H.U, V:Type
f:U -> V
H:~ (forall x y : U, f x = f y -> x = y)
exists x y : U, f x = f y /\ x <> y
    cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).U, V:Type
f:U -> V
H:~ (forall x y : U, f x = f y -> x = y)
(exists x : U, ~ (forall y : U, f x = f y -> x = y)) ->
exists x y : U, f x = f y /\ x <> y
U, V:Type
f:U -> V
H:~ (forall x y : U, f x = f y -> x = y)
exists x : U, ~ (forall y : U, f x = f y -> x = y)
    2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
      trivial with sets.U, V:Type
f:U -> V
H:~ (forall x y : U, f x = f y -> x = y)
(exists x : U, ~ (forall y : U, f x = f y -> x = y)) ->
exists x y : U, f x = f y /\ x <> y
    destruct 1 as [x C]; exists x.U, V:Type
f:U -> V
H:~ (forall x0 y : U, f x0 = f y -> x0 = y)
x:U
C:~ (forall y : U, f x = f y -> x = y)
exists y : U, f x = f y /\ x <> y
    cut (exists y : _, ~ (f x = f y -> x = y)).U, V:Type
f:U -> V
H:~ (forall x0 y : U, f x0 = f y -> x0 = y)
x:U
C:~ (forall y : U, f x = f y -> x = y)
(exists y : U, ~ (f x = f y -> x = y)) ->
exists y : U, f x = f y /\ x <> y
U, V:Type
f:U -> V
H:~ (forall x0 y : U, f x0 = f y -> x0 = y)
x:U
C:~ (forall y : U, f x = f y -> x = y)
exists y : U, ~ (f x = f y -> x = y)
    2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
      trivial with sets.U, V:Type
f:U -> V
H:~ (forall x0 y : U, f x0 = f y -> x0 = y)
x:U
C:~ (forall y : U, f x = f y -> x = y)
(exists y : U, ~ (f x = f y -> x = y)) ->
exists y : U, f x = f y /\ x <> y
    destruct 1 as [y D]; exists y.U, V:Type
f:U -> V
H:~ (forall x0 y0 : U, f x0 = f y0 -> x0 = y0)
x:U
C:~ (forall y0 : U, f x = f y0 -> x = y0)
y:U
D:~ (f x = f y -> x = y)
f x = f y /\ x <> y
    apply imply_to_and; trivial with sets.
  Qed.

  Lemma cardinal_Im_intro :
    forall (A:Ensemble U) (f:U -> V) (n:nat),
      cardinal _ A n ->  exists p : nat, cardinal _ (Im A f) p.U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
cardinal U A n ->
exists p : nat, cardinal V (Im A f) p
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
cardinal U A n ->
exists p : nat, cardinal V (Im A f) p
    intros.U, V:Type
A:Ensemble U
f:U -> V
n:nat
H:cardinal U A n
exists p : nat, cardinal V (Im A f) p
    apply finite_cardinal; apply finite_image.U, V:Type
A:Ensemble U
f:U -> V
n:nat
H:cardinal U A n
Finite U A
    apply cardinal_finite with n; trivial with sets.
  Qed.

  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.U, V:Type
forall (A : Ensemble U) (f : U -> V),
injective f ->
forall x : U, In V (Im A f) (f x) -> In U A x
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V),
injective f ->
forall x : U, In V (Im A f) (f x) -> In U A x
    intros.U, V:Type
A:Ensemble U
f:U -> V
H:injective f
x:U
H0:In V (Im A f) (f x)
In U A x
    elim Im_inv with A f (f x); trivial with sets.U, V:Type
A:Ensemble U
f:U -> V
H:injective f
x:U
H0:In V (Im A f) (f x)
forall x0 : U, In U A x0 /\ f x0 = f x -> In U A x
    intros z C; elim C; intros InAz E.U, V:Type
A:Ensemble U
f:U -> V
H:injective f
x:U
H0:In V (Im A f) (f x)
z:U
C:In U A z /\ f z = f x
InAz:In U A z
E:f z = f x
In U A x
    elim (H z x E); trivial with sets.
  Qed.

  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.U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
injective f ->
cardinal U A n ->
forall n' : nat, cardinal V (Im A f) n' -> n' = n
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
injective f ->
cardinal U A n ->
forall n' : nat, cardinal V (Im A f) n' -> n' = n
    induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.U, V:Type
f:U -> V
H:injective f
forall n' : nat,
cardinal V (Im (Empty_set U) f) n' -> n' = 0
U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' = n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' = S n
    rewrite (image_empty f).U, V:Type
f:U -> V
H:injective f
forall n' : nat, cardinal V (Empty_set V) n' -> n' = 0
U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' = n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' = S n
    intros n' CE.U, V:Type
f:U -> V
H:injective f
n':nat
CE:cardinal V (Empty_set V) n'
n' = 0
U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' = n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' = S n
    apply cardinal_unicity with V (Empty_set V); auto with sets.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' = n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' = S n
    intro n'.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
cardinal V (Im (Add U A x) f) n' -> n' = S n
    rewrite (Im_add A x f).U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
cardinal V (Add V (Im A f) (f x)) n' -> n' = S n
    intro H'3.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
n' = S n
    elim cardinal_Im_intro with A f n; trivial with sets.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
forall x0 : nat, cardinal V (Im A f) x0 -> n' = S n
    intros i CI.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
n' = S n
    lapply (H'1 i); trivial with sets.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
i = n -> n' = S n
    cut (~ In _ (Im A f) (f x)).U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
~ In V (Im A f) (f x) -> i = n -> n' = S n
U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
~ In V (Im A f) (f x)
    intros H0 H1.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
H0:~ In V (Im A f) (f x)
H1:i = n
n' = S n
U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
~ In V (Im A f) (f x)
    apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
H0:~ In V (Im A f) (f x)
H1:i = n
cardinal V (Add V (Im A f) (f x)) (S n)
U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
~ In V (Im A f) (f x)
    apply card_add; auto with sets.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
H0:~ In V (Im A f) (f x)
H1:i = n
cardinal V (Im A f) n
U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
~ In V (Im A f) (f x)
    rewrite <- H1; trivial with sets.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
~ In V (Im A f) (f x)
    red; intro; apply H'2.U, V:Type
f:U -> V
H:injective f
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 = n
n':nat
H'3:cardinal V (Add V (Im A f) (f x)) n'
i:nat
CI:cardinal V (Im A f) i
H0:In V (Im A f) (f x)
In U A x
    apply In_Image_elim with f; trivial with sets.
  Qed.

  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.U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
cardinal U A n ->
forall n' : nat, cardinal V (Im A f) n' -> n' <= n
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
cardinal U A n ->
forall n' : nat, cardinal V (Im A f) n' -> n' <= n
    induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.U, V:Type
f:U -> V
forall n' : nat,
cardinal V (Im (Empty_set U) f) n' -> n' <= 0
U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' <= n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' <= S n
    rewrite (image_empty f); intros.U, V:Type
f:U -> V
n':nat
H:cardinal V (Empty_set V) n'
n' <= 0
U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' <= n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' <= S n
    cut (n' = 0).U, V:Type
f:U -> V
n':nat
H:cardinal V (Empty_set V) n'
n' = 0 -> n' <= 0
U, V:Type
f:U -> V
n':nat
H:cardinal V (Empty_set V) n'
n' = 0
U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' <= n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' <= S n
    intro E; rewrite E; trivial with sets.U, V:Type
f:U -> V
n':nat
H:cardinal V (Empty_set V) n'
n' = 0
U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' <= n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' <= S n
    apply cardinal_unicity with V (Empty_set V); auto with sets.U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n' : nat, cardinal V (Im A f) n' -> n' <= n
forall n' : nat,
cardinal V (Im (Add U A x) f) n' -> n' <= S n
    intro n'.U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 <= n
n':nat
cardinal V (Im (Add U A x) f) n' -> n' <= S n
    rewrite (Im_add A x f).U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 <= n
n':nat
cardinal V (Add V (Im A f) (f x)) n' -> n' <= S n
    elim cardinal_Im_intro with A f n; trivial with sets.U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 <= n
n':nat
forall x0 : nat,
cardinal V (Im A f) x0 ->
cardinal V (Add V (Im A f) (f x)) n' -> n' <= S n
    intros p C H'3.U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 <= n
n', p:nat
C:cardinal V (Im A f) p
H'3:cardinal V (Add V (Im A f) (f x)) n'
n' <= S n
    apply le_trans with (S p).U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 <= n
n', p:nat
C:cardinal V (Im A f) p
H'3:cardinal V (Add V (Im A f) (f x)) n'
n' <= S p
U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 <= n
n', p:nat
C:cardinal V (Im A f) p
H'3:cardinal V (Add V (Im A f) (f x)) n'
S p <= S n
    apply card_Add_gen with V (Im A f) (f x); trivial with sets.U, V:Type
f:U -> V
A:Ensemble U
n:nat
H'0:cardinal U A n
x:U
H'2:~ In U A x
H'1:forall n'0 : nat, cardinal V (Im A f) n'0 -> n'0 <= n
n', p:nat
C:cardinal V (Im A f) p
H'3:cardinal V (Add V (Im A f) (f x)) n'
S p <= S n
    apply le_n_S; auto with sets.
  Qed.

  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.U, V:Type
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
  Proof.U, V:Type
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
    unfold not; intros A f n CAn n' CIfn' ltn'n I.U, V:Type
A:Ensemble U
f:U -> V
n:nat
CAn:cardinal U A n
n':nat
CIfn':cardinal V (Im A f) n'
ltn'n:n' < n
I:injective f
False
    cut (n' = n).U, V:Type
A:Ensemble U
f:U -> V
n:nat
CAn:cardinal U A n
n':nat
CIfn':cardinal V (Im A f) n'
ltn'n:n' < n
I:injective f
n' = n -> False
U, V:Type
A:Ensemble U
f:U -> V
n:nat
CAn:cardinal U A n
n':nat
CIfn':cardinal V (Im A f) n'
ltn'n:n' < n
I:injective f
n' = n
    intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).U, V:Type
A:Ensemble U
f:U -> V
n:nat
CAn:cardinal U A n
n':nat
CIfn':cardinal V (Im A f) n'
ltn'n:n' < n
I:injective f
n' = n
    apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
      trivial with sets.
  Qed.

  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).U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
cardinal U A n ->
forall n' : nat,
cardinal V (Im A f) n' ->
n' < n -> exists x y : U, f x = f y /\ x <> y
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V) (n : nat),
cardinal U A n ->
forall n' : nat,
cardinal V (Im A f) n' ->
n' < n -> exists x y : U, f x = f y /\ x <> y
    intros; apply not_injective_elim.U, V:Type
A:Ensemble U
f:U -> V
n:nat
H:cardinal U A n
n':nat
H0:cardinal V (Im A f) n'
H1:n' < n
~ injective f
    apply Pigeonhole with A n n'; trivial with sets.
  Qed.

End Image.

Hint Resolve Im_def image_empty finite_image: sets.