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.