Infinite_sets.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.
Require Export Image.

Section Approx.
  Variable U : Type.

  Inductive Approximant (A X:Ensemble U) : Prop :=
    Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
End Approx.

Hint Resolve Defn_of_Approximant : core.

Section Infinite_sets.
  Variable U : Type.

  Lemma make_new_approximant :
    forall A X:Ensemble U,
      ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).U:Type
forall A X : Ensemble U,
~ Finite U A ->
Approximant U A X -> Inhabited U (Setminus U A X)
  Proof.U:Type
forall A X : Ensemble U,
~ Finite U A ->
Approximant U A X -> Inhabited U (Setminus U A X)
    intros A X H' H'0.U:Type
A, X:Ensemble U
H':~ Finite U A
H'0:Approximant U A X
Inhabited U (Setminus U A X)
    elim H'0; intros H'1 H'2.U:Type
A, X:Ensemble U
H':~ Finite U A
H'0:Approximant U A X
H'1:Finite U X
H'2:Included U X A
Inhabited U (Setminus U A X)
    apply Strict_super_set_contains_new_element; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
H'0:Approximant U A X
H'1:Finite U X
H'2:Included U X A
X <> A
    red; intro H'3; apply H'.U:Type
A, X:Ensemble U
H':~ Finite U A
H'0:Approximant U A X
H'1:Finite U X
H'2:Included U X A
H'3:X = A
Finite U A
    rewrite <- H'3; auto with sets.
  Qed.

  Lemma approximants_grow :
    forall A X:Ensemble U,
      ~ Finite U A ->
      forall n:nat,
	cardinal U X n ->
	Included U X A ->  exists Y : _, cardinal U Y (S n) /\ Included U Y A.U:Type
forall A X : Ensemble U,
~ Finite U A ->
forall n : nat,
cardinal U X n ->
Included U X A ->
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
  Proof.U:Type
forall A X : Ensemble U,
~ Finite U A ->
forall n : nat,
cardinal U X n ->
Included U X A ->
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
    intros A X H' n H'0; elim H'0; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
Included U (Empty_set U) A ->
exists Y : Ensemble U,
  cardinal U Y 1 /\ Included U Y A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intro H'1.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
exists Y : Ensemble U,
  cardinal U Y 1 /\ Included U Y A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    cut (Inhabited U (Setminus U A (Empty_set U))).U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U)) ->
exists Y : Ensemble U,
  cardinal U Y 1 /\ Included U Y A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intro H'2; elim H'2.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
forall x : U,
In U (Setminus U A (Empty_set U)) x ->
exists Y : Ensemble U,
  cardinal U Y 1 /\ Included U Y A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intros x H'3.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
exists Y : Ensemble U,
  cardinal U Y 1 /\ Included U Y A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    exists (Add U (Empty_set U) x); auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
cardinal U (Add U (Empty_set U) x) 1 /\
Included U (Add U (Empty_set U) x) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    split.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
cardinal U (Add U (Empty_set U) x) 1
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
Included U (Add U (Empty_set U) x) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    apply card_add; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
Included U (Add U (Empty_set U) x) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    cut (In U A x).U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
In U A x -> Included U (Add U (Empty_set U) x) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
In U A x
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intro H'4; red; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
H'4:In U A x
forall x0 : U,
In U (Add U (Empty_set U) x) x0 -> In U A x0
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
In U A x
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intros x0 H'5; elim H'5; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
H'4:In U A x
x0:U
H'5:In U (Add U (Empty_set U) x) x0
forall x1 : U, In U (Singleton U x) x1 -> In U A x1
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
In U A x
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intros x1 H'6; elim H'6; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
H'2:Inhabited U (Setminus U A (Empty_set U))
x:U
H'3:In U (Setminus U A (Empty_set U)) x
In U A x
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    elim H'3; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Included U (Empty_set U) A
Inhabited U (Setminus U A (Empty_set U))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    apply make_new_approximant; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
forall (A0 : Ensemble U) (n0 : nat),
cardinal U A0 n0 ->
(Included U A0 A ->
 exists Y : Ensemble U,
   cardinal U Y (S n0) /\ Included U Y A) ->
forall x : U,
~ In U A0 x ->
Included U (Add U A0 x) A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intros A0 n0 H'1 H'2 x H'3 H'5.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
H'2:Included U A0 A ->
exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
forall x0 : Ensemble U,
cardinal U x0 (S n0) /\ Included U x0 A ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    intros x0 H'2; try assumption.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'2:cardinal U x0 (S n0) /\ Included U x0 A
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    elim H'2; intros H'7 H'8; try exact H'8; clear H'2.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
    elim (make_new_approximant A x0); auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
forall x1 : U,
In U (Setminus U A x0) x1 ->
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    intros x1 H'2; try assumption.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
exists Y : Ensemble U,
  cardinal U Y (S (S n0)) /\ Included U Y A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    exists (Add U x0 x1); auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
cardinal U (Add U x0 x1) (S (S n0)) /\
Included U (Add U x0 x1) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    split.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
cardinal U (Add U x0 x1) (S (S n0))
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
Included U (Add U x0 x1) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    apply card_add; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
~ In U x0 x1
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
Included U (Add U x0 x1) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    elim H'2; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
Included U (Add U x0 x1) A
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    red.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
forall x2 : U, In U (Add U x0 x1) x2 -> In U A x2
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    intros x2 H'9; elim H'9; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
x2:U
H'9:In U (Add U x0 x1) x2
forall x3 : U, In U (Singleton U x1) x3 -> In U A x3
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    intros x3 H'10; elim H'10; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
x1:U
H'2:In U (Setminus U A x0) x1
x2:U
H'9:In U (Add U x0 x1) x2
x3:U
H'10:In U (Singleton U x1) x3
In U A x1
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U,
  cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    elim H'2; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Approximant U A x0
    apply Defn_of_Approximant; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
A0:Ensemble U
n0:nat
H'1:cardinal U A0 n0
x:U
H'3:~ In U A0 x
H'5:Included U (Add U A0 x) A
H'6:exists Y : Ensemble U, cardinal U Y (S n0) /\ Included U Y A
x0:Ensemble U
H'7:cardinal U x0 (S n0)
H'8:Included U x0 A
Finite U x0
    apply cardinal_finite with (n := S n0); auto with sets.
  Qed.

  Lemma approximants_grow' :
    forall A X:Ensemble U,
      ~ Finite U A ->
      forall n:nat,
	cardinal U X n ->
	Approximant U A X ->
	exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.U:Type
forall A X : Ensemble U,
~ Finite U A ->
forall n : nat,
cardinal U X n ->
Approximant U A X ->
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Approximant U A Y
  Proof.U:Type
forall A X : Ensemble U,
~ Finite U A ->
forall n : nat,
cardinal U X n ->
Approximant U A X ->
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Approximant U A Y
    intros A X H' n H'0 H'1; try assumption.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Approximant U A Y
    elim H'1.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
Finite U X ->
Included U X A ->
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Approximant U A Y
    intros H'2 H'3.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Approximant U A Y
    elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
forall x : Ensemble U,
cardinal U x (S n) /\ Included U x A ->
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Approximant U A Y
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
    intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
x:Ensemble U
H'5:cardinal U x (S n)
H'6:Included U x A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Approximant U A Y
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
    exists x; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
x:Ensemble U
H'5:cardinal U x (S n)
H'6:Included U x A
cardinal U x (S n) /\ Approximant U A x
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
    split; [ auto with sets | idtac ].U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
x:Ensemble U
H'5:cardinal U x (S n)
H'6:Included U x A
Approximant U A x
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
    apply Defn_of_Approximant; auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
x:Ensemble U
H'5:cardinal U x (S n)
H'6:Included U x A
Finite U x
U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
    apply cardinal_finite with (n := S n); auto with sets.U:Type
A, X:Ensemble U
H':~ Finite U A
n:nat
H'0:cardinal U X n
H'1:Approximant U A X
H'2:Finite U X
H'3:Included U X A
exists Y : Ensemble U,
  cardinal U Y (S n) /\ Included U Y A
    apply approximants_grow with (X := X); auto with sets.
  Qed.

  Lemma approximant_can_be_any_size :
    forall A X:Ensemble U,
      ~ Finite U A ->
      forall n:nat,  exists Y : _, cardinal U Y n /\ Approximant U A Y.U:Type
forall A : Ensemble U,
Ensemble U ->
~ Finite U A ->
forall n : nat,
exists Y : Ensemble U,
  cardinal U Y n /\ Approximant U A Y
  Proof.U:Type
forall A : Ensemble U,
Ensemble U ->
~ Finite U A ->
forall n : nat,
exists Y : Ensemble U,
  cardinal U Y n /\ Approximant U A Y
    intros A H' H'0 n; elim n.U:Type
A, H':Ensemble U
H'0:~ Finite U A
n:nat
exists Y : Ensemble U,
  cardinal U Y 0 /\ Approximant U A Y
U:Type
A, H':Ensemble U
H'0:~ Finite U A
n:nat
forall n0 : nat,
(exists Y : Ensemble U,
   cardinal U Y n0 /\ Approximant U A Y) ->
exists Y : Ensemble U,
  cardinal U Y (S n0) /\ Approximant U A Y
    exists (Empty_set U); auto with sets.U:Type
A, H':Ensemble U
H'0:~ Finite U A
n:nat
forall n0 : nat,
(exists Y : Ensemble U,
   cardinal U Y n0 /\ Approximant U A Y) ->
exists Y : Ensemble U,
  cardinal U Y (S n0) /\ Approximant U A Y
    intros n0 H'1; elim H'1.U:Type
A, H':Ensemble U
H'0:~ Finite U A
n, n0:nat
H'1:exists Y : Ensemble U, cardinal U Y n0 /\ Approximant U A Y
forall x : Ensemble U,
cardinal U x n0 /\ Approximant U A x ->
exists Y : Ensemble U,
  cardinal U Y (S n0) /\ Approximant U A Y
    intros x H'2.U:Type
A, H':Ensemble U
H'0:~ Finite U A
n, n0:nat
H'1:exists Y : Ensemble U, cardinal U Y n0 /\ Approximant U A Y
x:Ensemble U
H'2:cardinal U x n0 /\ Approximant U A x
exists Y : Ensemble U,
  cardinal U Y (S n0) /\ Approximant U A Y
    apply approximants_grow' with (X := x); tauto.
  Qed.

  Variable V : Type.

  Theorem Image_set_continuous :
    forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
      Finite V X ->
      Included V X (Im U V A f) ->
      exists n : _,
	(exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).U, V:Type
forall (A : Ensemble U) (f : U -> V) (X : Ensemble V),
Finite V X ->
Included V X (Im U V A f) ->
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V) (X : Ensemble V),
Finite V X ->
Included V X (Im U V A f) ->
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    intros A f X H'; elim H'.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
Included V (Empty_set V) (Im U V A f) ->
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = Empty_set V
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
forall A0 : Ensemble V,
Finite V A0 ->
(Included V A0 (Im U V A f) ->
 exists (n : nat) (Y : Ensemble U),
   (cardinal U Y n /\ Included U Y A) /\
   Im U V Y f = A0) ->
forall x : V,
~ In V A0 x ->
Included V (Add V A0 x) (Im U V A f) ->
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    intro H'0; exists 0.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
H'0:Included V (Empty_set V) (Im U V A f)
exists Y : Ensemble U,
  (cardinal U Y 0 /\ Included U Y A) /\
  Im U V Y f = Empty_set V
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
forall A0 : Ensemble V,
Finite V A0 ->
(Included V A0 (Im U V A f) ->
 exists (n : nat) (Y : Ensemble U),
   (cardinal U Y n /\ Included U Y A) /\
   Im U V Y f = A0) ->
forall x : V,
~ In V A0 x ->
Included V (Add V A0 x) (Im U V A f) ->
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    exists (Empty_set U); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
forall A0 : Ensemble V,
Finite V A0 ->
(Included V A0 (Im U V A f) ->
 exists (n : nat) (Y : Ensemble U),
   (cardinal U Y n /\ Included U Y A) /\
   Im U V Y f = A0) ->
forall x : V,
~ In V A0 x ->
Included V (Add V A0 x) (Im U V A f) ->
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    intros A0 H'0 H'1 x H'2 H'3; try assumption.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
H'1:Included V A0 (Im U V A f) ->
exists (n : nat) (Y : Ensemble U),
(cardinal U Y n /\ Included U Y A) /\ Im U V Y f = A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    lapply H'1;
      [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
      auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = A0
forall x0 : Ensemble U,
(cardinal U x0 n /\ Included U x0 A) /\
Im U V x0 f = A0 ->
exists (n0 : nat) (Y : Ensemble U),
  (cardinal U Y n0 /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    intros x0 H'1; try assumption.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = A0
x0:Ensemble U
H'1:(cardinal U x0 n /\ Included U x0 A) /\ Im U V x0 f = A0
exists (n0 : nat) (Y : Ensemble U),
  (cardinal U Y n0 /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    exists (S n); try assumption.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = A0
x0:Ensemble U
H'1:(cardinal U x0 n /\ Included U x0 A) /\ Im U V x0 f = A0
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
      clear H'4 H'1.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = A0
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    clear E.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    generalize H'2.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
~ In V A0 x ->
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V A0 x
    rewrite <- H'5.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
~ In V (Im U V x0 f) x ->
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V (Im U V x0 f) x
    intro H'1; try assumption.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:Included V (Add V A0 x) (Im U V A f)
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V (Im U V x0 f) x
    red in H'3.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x1 : V, In V (Add V A0 x) x1 -> In V (Im U V A f) x1
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V (Im U V x0 f) x
    generalize (H'3 x).U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x1 : V, In V (Add V A0 x) x1 -> In V (Im U V A f) x1
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
(In V (Add V A0 x) x -> In V (Im U V A f) x) ->
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V (Im U V x0 f) x
    intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
      auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x1 : V, In V (Add V A0 x) x1 -> In V (Im U V A f) x1
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V (Im U V x0 f) x
    specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
      intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
	auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x1 : V, In V (Add V A0 x) x1 -> In V (Im U V A f) x1
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x1 : U, In U A x1 /\ f x1 = x
forall x1 : U,
In U A x1 /\ f x1 = x ->
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V (Im U V x0 f) x
    intros x1 H'4; try assumption.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
exists Y : Ensemble U,
  (cardinal U Y (S n) /\ Included U Y A) /\
  Im U V Y f = Add V (Im U V x0 f) x
    apply ex_intro with (x := Add U x0 x1).U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
(cardinal U (Add U x0 x1) (S n) /\
 Included U (Add U x0 x1) A) /\
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    split; [ split; [ try assumption | idtac ] | idtac ].U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
cardinal U (Add U x0 x1) (S n)
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Included U (Add U x0 x1) A
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    apply card_add; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
~ In U x0 x1
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Included U (Add U x0 x1) A
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    red; intro H'9; try exact H'9.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
H'9:In U x0 x1
False
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Included U (Add U x0 x1) A
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    apply H'1.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
H'9:In U x0 x1
In V (Im U V x0 f) x
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Included U (Add U x0 x1) A
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Included U (Add U x0 x1) A
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'9:In U A x1
H'10:f x1 = x
Included U (Add U x0 x1) A
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    red; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'9:In U A x1
H'10:f x1 = x
forall x2 : U, In U (Add U x0 x1) x2 -> In U A x2
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    intros x2 H'4; elim H'4; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x3 : V, In V (Add V A0 x) x3 -> In V (Im U V A f) x3
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x3 : U, In U A x3 /\ f x3 = x
x1:U
H'9:In U A x1
H'10:f x1 = x
x2:U
H'4:In U (Add U x0 x1) x2
forall x3 : U, In U (Singleton U x1) x3 -> In U A x3
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V,
In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    intros x3 H'11; elim H'11; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'4:In U A x1 /\ f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) x
    elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Finite V X
A0:Ensemble V
H'0:Finite V A0
x:V
H'2:~ In V A0 x
H'3:forall x2 : V, In V (Add V A0 x) x2 -> In V (Im U V A f) x2
n:nat
x0:Ensemble U
H'5:Im U V x0 f = A0
H'6:cardinal U x0 n
H'7:Included U x0 A
H'1:~ In V (Im U V x0 f) x
H'8:In V (Im U V A f) x
H'13:exists x2 : U, In U A x2 /\ f x2 = x
x1:U
H'9:In U A x1
H'10:f x1 = x
Im U V (Add U x0 x1) f = Add V (Im U V x0 f) (f x1)
    apply Im_add; auto with sets.
  Qed.

  Theorem Image_set_continuous' :
    forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
      Approximant V (Im U V A f) X ->
      exists Y : _, Approximant U A Y /\ Im U V Y f = X.U, V:Type
forall (A : Ensemble U) (f : U -> V) (X : Ensemble V),
Approximant V (Im U V A f) X ->
exists Y : Ensemble U,
  Approximant U A Y /\ Im U V Y f = X
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V) (X : Ensemble V),
Approximant V (Im U V A f) X ->
exists Y : Ensemble U,
  Approximant U A Y /\ Im U V Y f = X
    intros A f X H'; try assumption.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists Y : Ensemble U,
  Approximant U A Y /\ Im U V Y f = X
    cut
      (exists n : _,
	(exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
(exists (n : nat) (Y : Ensemble U),
   (cardinal U Y n /\ Included U Y A) /\
   Im U V Y f = X) ->
exists Y : Ensemble U,
  Approximant U A Y /\ Im U V Y f = X
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    intro H'0; elim H'0; intros n E; elim E; clear H'0.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = X
forall x : Ensemble U,
(cardinal U x n /\ Included U x A) /\ Im U V x f = X ->
exists Y : Ensemble U,
  Approximant U A Y /\ Im U V Y f = X
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    intros x H'0; try assumption.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = X
x:Ensemble U
H'0:(cardinal U x n /\ Included U x A) /\ Im U V x f = X
exists Y : Ensemble U,
  Approximant U A Y /\ Im U V Y f = X
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
      clear H'1 H'0; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = X
x:Ensemble U
H'2:Im U V x f = X
H'3:cardinal U x n
H'4:Included U x A
exists Y : Ensemble U,
  Approximant U A Y /\ Im U V Y f = X
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    exists x.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = X
x:Ensemble U
H'2:Im U V x f = X
H'3:cardinal U x n
H'4:Included U x A
Approximant U A x /\ Im U V x f = X
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    split; [ idtac | try assumption ].U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = X
x:Ensemble U
H'2:Im U V x f = X
H'3:cardinal U x n
H'4:Included U x A
Approximant U A x
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    apply Defn_of_Approximant; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
n:nat
E:exists Y : Ensemble U,
  (cardinal U Y n /\ Included U Y A) /\
  Im U V Y f = X
x:Ensemble U
H'2:Im U V x f = X
H'3:cardinal U x n
H'4:Included U x A
Finite U x
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    apply cardinal_finite with (n := n); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
exists (n : nat) (Y : Ensemble U),
  (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X
    apply Image_set_continuous; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
Finite V X
U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
Included V X (Im U V A f)
    elim H'; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
X:Ensemble V
H':Approximant V (Im U V A f) X
Included V X (Im U V A f)
    elim H'; auto with sets.
  Qed.

  Theorem Pigeonhole_bis :
    forall (A:Ensemble U) (f:U -> V),
      ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.U, V:Type
forall (A : Ensemble U) (f : U -> V),
~ Finite U A ->
Finite V (Im U V A f) -> ~ injective U V f
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V),
~ Finite U A ->
Finite V (Im U V A f) -> ~ injective U V f
    intros A f H'0 H'1; try assumption.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
~ injective U V f
    elim (Image_set_continuous' A f (Im U V A f)); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
forall x : Ensemble U,
Approximant U A x /\ Im U V x f = Im U V A f ->
~ injective U V f
    intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
~ injective U V f
    elim (make_new_approximant A x); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
forall x0 : U,
In U (Setminus U A x) x0 -> ~ injective U V f
    intros x0 H'2; elim H'2.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
In U A x0 -> ~ In U x x0 -> ~ injective U V f
    intros H'5 H'6.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
~ injective U V f
    elim (finite_cardinal V (Im U V A f)); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
forall x1 : nat,
cardinal V (Im U V A f) x1 -> ~ injective U V f
    intros n E.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
~ injective U V f
    elim (finite_cardinal U x); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
forall x1 : nat, cardinal U x x1 -> ~ injective U V f
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    intros n0 E0.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
~ injective U V f
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
cardinal U (Add U x x0) (S n0)
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
cardinal V (Im U V (Add U x x0) f) n
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    apply card_add; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
cardinal V (Im U V (Add U x x0) f) n
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    rewrite (Im_add U V x x0 f); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
cardinal V (Add V (Im U V x f) (f x0)) n
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    cut (In V (Im U V x f) (f x0)).U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
In V (Im U V x f) (f x0) ->
cardinal V (Add V (Im U V x f) (f x0)) n
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
In V (Im U V x f) (f x0)
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    intro H'8.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
H'8:In V (Im U V x f) (f x0)
cardinal V (Add V (Im U V x f) (f x0)) n
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
In V (Im U V x f) (f x0)
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
H'8:In V (Im U V x f) (f x0)
cardinal V (Im U V x f) n
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
In V (Im U V x f) (f x0)
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    rewrite H'4; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
In V (Im U V x f) (f x0)
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n < S n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    apply le_lt_n_Sm.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
n <= n0
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
      auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
n0:nat
E0:cardinal U x n0
cardinal V (Im U V x f) n
U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    rewrite H'4; auto with sets.U, V:Type
A:Ensemble U
f:U -> V
H'0:~ Finite U A
H'1:Finite V (Im U V A f)
x:Ensemble U
H'3:Approximant U A x
H'4:Im U V x f = Im U V A f
x0:U
H'2:In U (Setminus U A x) x0
H'5:In U A x0
H'6:~ In U x x0
n:nat
E:cardinal V (Im U V A f) n
Finite U x
    elim H'3; auto with sets.
  Qed.

  Theorem Pigeonhole_ter :
    forall (A:Ensemble U) (f:U -> V) (n:nat),
      injective U V f -> Finite V (Im U V A f) -> Finite U A.U, V:Type
forall (A : Ensemble U) (f : U -> V),
nat ->
injective U V f -> Finite V (Im U V A f) -> Finite U A
  Proof.U, V:Type
forall (A : Ensemble U) (f : U -> V),
nat ->
injective U V f -> Finite V (Im U V A f) -> Finite U A
    intros A f H' H'0 H'1.U, V:Type
A:Ensemble U
f:U -> V
H':nat
H'0:injective U V f
H'1:Finite V (Im U V A f)
Finite U A
    apply NNPP.U, V:Type
A:Ensemble U
f:U -> V
H':nat
H'0:injective U V f
H'1:Finite V (Im U V A f)
~ ~ Finite U A
    red; intro H'2.U, V:Type
A:Ensemble U
f:U -> V
H':nat
H'0:injective U V f
H'1:Finite V (Im U V A f)
H'2:~ Finite U A
False
    elim (Pigeonhole_bis A f); auto with sets.
  Qed.

End Infinite_sets.