# Library Coq.Sets.Infinite_sets

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
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.
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).
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.
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.
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.
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 ).
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.
Theorem Pigeonhole_bis :
forall (A:Ensemble U) (f:U -> V),
~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
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.
End Infinite_sets.