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).
Proof.
intros A X H' H'0.
elim H'0; intros H'1 H'2.
apply Strict_super_set_contains_new_element; auto with sets.
red in |- *; intro H'3; apply H'.
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.
Proof.
intros A X H' n H'0; elim H'0; auto with sets.
intro H'1.
cut (Inhabited U (Setminus U A (Empty_set U))).
intro H'2; elim H'2.
intros x H'3.
exists (Add U (Empty_set U) x); auto with sets.
split.
apply card_add; auto with sets.
cut (In U A x).
intro H'4; red in |- *; auto with sets.
intros x0 H'5; elim H'5; auto with sets.
intros x1 H'6; elim H'6; auto with sets.
elim H'3; auto with sets.
apply make_new_approximant; auto with sets.
intros A0 n0 H'1 H'2 x H'3 H'5.
lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
intros x0 H'2; try assumption.
elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
elim (make_new_approximant A x0); auto with sets.
intros x1 H'2; try assumption.
exists (Add U x0 x1); auto with sets.
split.
apply card_add; auto with sets.
elim H'2; auto with sets.
red in |- *.
intros x2 H'9; elim H'9; auto with sets.
intros x3 H'10; elim H'10; auto with sets.
elim H'2; auto with sets.
auto with sets.
apply Defn_of_Approximant; auto with sets.
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.
Proof.
intros A X H' n H'0 H'1; try assumption.
elim H'1.
intros H'2 H'3.
elimtype (exists Y : _, 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.
exists x; auto with sets.
split; [ auto with sets | idtac ].
apply Defn_of_Approximant; auto with sets.
apply cardinal_finite with (n := S n); auto with sets.
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.
Proof.
intros A H' H'0 n; elim n.
exists (Empty_set U); auto with sets.
intros n0 H'1; elim H'1.
intros x H'2.
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).
Proof.
intros A f X H'; elim H'.
intro H'0; exists 0.
exists (Empty_set U); auto with sets.
intros A0 H'0 H'1 x H'2 H'3; try assumption.
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.
intros x0 H'1; try assumption.
exists (S n); try assumption.
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.
clear E.
generalize H'2.
rewrite <- H'5.
intro H'1; try assumption.
red in H'3.
generalize (H'3 x).
intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
auto with sets.
specialize 5Im_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.
intros x1 H'4; try assumption.
apply ex_intro with (x := Add U x0 x1).
split; [ split; [ try assumption | idtac ] | idtac ].
apply card_add; auto with sets.
red in |- *; intro H'9; try exact H'9.
apply H'1.
elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
red in |- *; auto with sets.
intros x2 H'4; elim H'4; auto with sets.
intros x3 H'11; elim H'11; auto with sets.
elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
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.
Proof.
intros A f X H'; try assumption.
cut
(exists n : _,
(exists Y : _, (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.
intros x H'0; try assumption.
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.
exists x.
split; [ idtac | try assumption ].
apply Defn_of_Approximant; auto with sets.
apply cardinal_finite with (n := n); auto with sets.
apply Image_set_continuous; auto with sets.
elim H'; auto with sets.
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.
Proof.
intros A f H'0 H'1; try assumption.
elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
elim (make_new_approximant A x); auto with sets.
intros x0 H'2; elim H'2.
intros H'5 H'6.
elim (finite_cardinal V (Im U V A f)); auto with sets.
intros n E.
elim (finite_cardinal U x); auto with sets.
intros n0 E0.
apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
apply card_add; auto with sets.
rewrite (Im_add U V x x0 f); auto with sets.
cut (In V (Im U V x f) (f x0)).
intro H'8.
rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
rewrite H'4; auto with sets.
elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
apply le_lt_n_Sm.
apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
auto with sets.
rewrite H'4; auto with sets.
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.
Proof.
intros A f H' H'0 H'1.
apply NNPP.
red in |- *; intro H'2.
elim (Pigeonhole_bis A f); auto with sets.
Qed.
End Infinite_sets.