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.