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: Image.v 9245 2006-10-17 12:53:34Z notin $ 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.
44
Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
45
Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y.
48
forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
50
intros X f x H'; try assumption.
51
apply Im_intro with (x := x); auto with sets.
55
forall (X:Ensemble U) (x:U) (f:U -> V),
56
Im (Add _ X x) f = Add _ (Im X f) (f x).
59
apply Extensionality_Ensembles.
60
split; red in |- *; intros x0 H'.
63
elim Add_inv with U X x x1; auto using Im_def with sets.
64
destruct 1; auto using Im_def with sets.
65
elim Add_inv with V (Im X f) (f x) x0.
66
destruct 1 as [x0 H y H0].
67
rewrite H0; auto using Im_def with sets.
68
destruct 1; auto using Im_def with sets.
72
Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
74
intro f; try assumption.
75
apply Extensionality_Ensembles.
76
split; auto with sets.
79
intros x0 H'0; elim H'0; auto with sets.
83
forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
85
intros X f H'; elim H'.
86
rewrite (image_empty f); auto with sets.
87
intros A H'0 H'1 x H'2; clear H' X.
88
rewrite (Im_add A x f); auto with sets.
89
apply Add_preserves_Finite; auto with sets.
93
forall (X:Ensemble U) (f:U -> V) (y:V),
94
In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y.
96
intros X f y H'; elim H'.
97
intros x H'0 y0 H'1; rewrite H'1.
98
exists x; auto with sets.
101
Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
103
Lemma not_injective_elim :
105
~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y).
107
unfold injective in |- *; intros f H.
108
cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
109
2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
111
destruct 1 as [x C]; exists x.
112
cut (exists y : _, ~ (f x = f y -> x = y)).
113
2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
115
destruct 1 as [y D]; exists y.
116
apply imply_to_and; trivial with sets.
119
Lemma cardinal_Im_intro :
120
forall (A:Ensemble U) (f:U -> V) (n:nat),
121
cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p.
124
apply finite_cardinal; apply finite_image.
125
apply cardinal_finite with n; trivial with sets.
128
Lemma In_Image_elim :
129
forall (A:Ensemble U) (f:U -> V),
130
injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
133
elim Im_inv with A f (f x); trivial with sets.
134
intros z C; elim C; intros InAz E.
135
elim (H z x E); trivial with sets.
138
Lemma injective_preserves_cardinal :
139
forall (A:Ensemble U) (f:U -> V) (n:nat),
141
cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
143
induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.
144
rewrite (image_empty f).
146
apply cardinal_unicity with V (Empty_set V); auto with sets.
148
rewrite (Im_add A x f).
150
elim cardinal_Im_intro with A f n; trivial with sets.
152
lapply (H'1 i); trivial with sets.
153
cut (~ In _ (Im A f) (f x)).
155
apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
156
apply card_add; auto with sets.
157
rewrite <- H1; trivial with sets.
158
red in |- *; intro; apply H'2.
159
apply In_Image_elim with f; trivial with sets.
162
Lemma cardinal_decreases :
163
forall (A:Ensemble U) (f:U -> V) (n:nat),
164
cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
166
induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.
167
rewrite (image_empty f); intros.
169
intro E; rewrite E; trivial with sets.
170
apply cardinal_unicity with V (Empty_set V); auto with sets.
172
rewrite (Im_add A x f).
173
elim cardinal_Im_intro with A f n; trivial with sets.
175
apply le_trans with (S p).
176
apply card_Add_gen with V (Im A f) (f x); trivial with sets.
177
apply le_n_S; auto with sets.
181
forall (A:Ensemble U) (f:U -> V) (n:nat),
183
forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
185
unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
187
intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
188
apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
192
Lemma Pigeonhole_principle :
193
forall (A:Ensemble U) (f:U -> V) (n:nat),
196
cardinal _ (Im A f) n' ->
197
n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y).
199
intros; apply not_injective_elim.
200
apply Pigeonhole with A n n'; trivial with sets.
205
Hint Resolve Im_def image_empty finite_image: sets v62.
b'\\ No newline at end of file'