# Library Coq.Sets.Infinite_sets

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Finite_sets_facts.
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.

#[global]
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).

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.