1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(****************************************************************************)
10
(* Naive Set Theory in Coq *)
13
(* Rocquencourt Sophia-Antipolis *)
22
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
23
(* to the Newton Institute for providing an exceptional work environment *)
24
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
25
(****************************************************************************)
27
(*i $Id: Infinite_sets.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
29
Require Export Finite_sets.
30
Require Export Constructive_sets.
31
Require Export Classical_Type.
32
Require Export Classical_sets.
33
Require Export Powerset.
34
Require Export Powerset_facts.
35
Require Export Powerset_Classical_facts.
39
Require Export Finite_sets_facts.
45
Inductive Approximant (A X:Ensemble U) : Prop :=
46
Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
49
Hint Resolve Defn_of_Approximant.
51
Section Infinite_sets.
54
Lemma make_new_approximant :
55
forall A X:Ensemble U,
56
~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
59
elim H'0; intros H'1 H'2.
60
apply Strict_super_set_contains_new_element; auto with sets.
61
red in |- *; intro H'3; apply H'.
62
rewrite <- H'3; auto with sets.
65
Lemma approximants_grow :
66
forall A X:Ensemble U,
70
Included U X A -> exists Y : _, cardinal U Y (S n) /\ Included U Y A.
72
intros A X H' n H'0; elim H'0; auto with sets.
74
cut (Inhabited U (Setminus U A (Empty_set U))).
77
exists (Add U (Empty_set U) x); auto with sets.
79
apply card_add; auto with sets.
81
intro H'4; red in |- *; auto with sets.
82
intros x0 H'5; elim H'5; auto with sets.
83
intros x1 H'6; elim H'6; auto with sets.
84
elim H'3; auto with sets.
85
apply make_new_approximant; auto with sets.
86
intros A0 n0 H'1 H'2 x H'3 H'5.
87
lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
88
intros x0 H'2; try assumption.
89
elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
90
elim (make_new_approximant A x0); auto with sets.
91
intros x1 H'2; try assumption.
92
exists (Add U x0 x1); auto with sets.
94
apply card_add; auto with sets.
95
elim H'2; auto with sets.
97
intros x2 H'9; elim H'9; auto with sets.
98
intros x3 H'10; elim H'10; auto with sets.
99
elim H'2; auto with sets.
101
apply Defn_of_Approximant; auto with sets.
102
apply cardinal_finite with (n := S n0); auto with sets.
105
Lemma approximants_grow' :
106
forall A X:Ensemble U,
111
exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
113
intros A X H' n H'0 H'1; try assumption.
116
elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).
117
intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
118
exists x; auto with sets.
119
split; [ auto with sets | idtac ].
120
apply Defn_of_Approximant; auto with sets.
121
apply cardinal_finite with (n := S n); auto with sets.
122
apply approximants_grow with (X := X); auto with sets.
125
Lemma approximant_can_be_any_size :
126
forall A X:Ensemble U,
128
forall n:nat, exists Y : _, cardinal U Y n /\ Approximant U A Y.
130
intros A H' H'0 n; elim n.
131
exists (Empty_set U); auto with sets.
132
intros n0 H'1; elim H'1.
134
apply approximants_grow' with (X := x); tauto.
139
Theorem Image_set_continuous :
140
forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
142
Included V X (Im U V A f) ->
144
(exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
146
intros A f X H'; elim H'.
148
exists (Empty_set U); auto with sets.
149
intros A0 H'0 H'1 x H'2 H'3; try assumption.
151
[ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
153
intros x0 H'1; try assumption.
154
exists (S n); try assumption.
155
elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
160
intro H'1; try assumption.
163
intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
165
specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
166
intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
168
intros x1 H'4; try assumption.
169
apply ex_intro with (x := Add U x0 x1).
170
split; [ split; [ try assumption | idtac ] | idtac ].
171
apply card_add; auto with sets.
172
red in |- *; intro H'9; try exact H'9.
174
elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
175
elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
176
red in |- *; auto with sets.
177
intros x2 H'4; elim H'4; auto with sets.
178
intros x3 H'11; elim H'11; auto with sets.
179
elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
180
apply Im_add; auto with sets.
183
Theorem Image_set_continuous' :
184
forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
185
Approximant V (Im U V A f) X ->
186
exists Y : _, Approximant U A Y /\ Im U V Y f = X.
188
intros A f X H'; try assumption.
191
(exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
192
intro H'0; elim H'0; intros n E; elim E; clear H'0.
193
intros x H'0; try assumption.
194
elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
195
clear H'1 H'0; auto with sets.
197
split; [ idtac | try assumption ].
198
apply Defn_of_Approximant; auto with sets.
199
apply cardinal_finite with (n := n); auto with sets.
200
apply Image_set_continuous; auto with sets.
201
elim H'; auto with sets.
202
elim H'; auto with sets.
205
Theorem Pigeonhole_bis :
206
forall (A:Ensemble U) (f:U -> V),
207
~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
209
intros A f H'0 H'1; try assumption.
210
elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
211
intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
212
elim (make_new_approximant A x); auto with sets.
213
intros x0 H'2; elim H'2.
215
elim (finite_cardinal V (Im U V A f)); auto with sets.
217
elim (finite_cardinal U x); auto with sets.
219
apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
220
apply card_add; auto with sets.
221
rewrite (Im_add U V x x0 f); auto with sets.
222
cut (In V (Im U V x f) (f x0)).
224
rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
225
rewrite H'4; auto with sets.
226
elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
228
apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
230
rewrite H'4; auto with sets.
231
elim H'3; auto with sets.
234
Theorem Pigeonhole_ter :
235
forall (A:Ensemble U) (f:U -> V) (n:nat),
236
injective U V f -> Finite V (Im U V A f) -> Finite U A.
238
intros A f H' H'0 H'1.
240
red in |- *; intro H'2.
241
elim (Pigeonhole_bis A f); auto with sets.