diff options
Diffstat (limited to 'theories/Sets/Image.v')
| -rw-r--r-- | theories/Sets/Image.v | 322 |
1 files changed, 161 insertions, 161 deletions
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index c97aa127..d3591acf 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Image.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Image.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Finite_sets. Require Export Constructive_sets. @@ -39,167 +39,167 @@ Require Export Le. Require Export Finite_sets_facts. Section Image. -Variables U V : Type. - -Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V := + Variables U V : Type. + + Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V := Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y. + + Lemma Im_def : + forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x). + Proof. + intros X f x H'; try assumption. + apply Im_intro with (x := x); auto with sets. + Qed. + + Lemma Im_add : + forall (X:Ensemble U) (x:U) (f:U -> V), + Im (Add _ X x) f = Add _ (Im X f) (f x). + Proof. + intros X x f. + apply Extensionality_Ensembles. + split; red in |- *; intros x0 H'. + elim H'; intros. + rewrite H0. + elim Add_inv with U X x x1; auto using Im_def with sets. + destruct 1; auto using Im_def with sets. + elim Add_inv with V (Im X f) (f x) x0. + destruct 1 as [x0 H y H0]. + rewrite H0; auto using Im_def with sets. + destruct 1; auto using Im_def with sets. + trivial. + Qed. + + Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V. + Proof. + intro f; try assumption. + apply Extensionality_Ensembles. + split; auto with sets. + red in |- *. + intros x H'; elim H'. + intros x0 H'0; elim H'0; auto with sets. + Qed. + + Lemma finite_image : + forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f). + Proof. + intros X f H'; elim H'. + rewrite (image_empty f); auto with sets. + intros A H'0 H'1 x H'2; clear H' X. + rewrite (Im_add A x f); auto with sets. + apply Add_preserves_Finite; auto with sets. + Qed. + + Lemma Im_inv : + forall (X:Ensemble U) (f:U -> V) (y:V), + In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y. + Proof. + intros X f y H'; elim H'. + intros x H'0 y0 H'1; rewrite H'1. + exists x; auto with sets. + Qed. + + Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. + + Lemma not_injective_elim : + forall f:U -> V, + ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y). + Proof. + unfold injective in |- *; intros f H. + cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)). + 2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); + trivial with sets. + destruct 1 as [x C]; exists x. + cut (exists y : _, ~ (f x = f y -> x = y)). + 2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y); + trivial with sets. + destruct 1 as [y D]; exists y. + apply imply_to_and; trivial with sets. + Qed. + + Lemma cardinal_Im_intro : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p. + Proof. + intros. + apply finite_cardinal; apply finite_image. + apply cardinal_finite with n; trivial with sets. + Qed. + + Lemma In_Image_elim : + forall (A:Ensemble U) (f:U -> V), + injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x. + Proof. + intros. + elim Im_inv with A f (f x); trivial with sets. + intros z C; elim C; intros InAz E. + elim (H z x E); trivial with sets. + Qed. + + Lemma injective_preserves_cardinal : + forall (A:Ensemble U) (f:U -> V) (n:nat), + injective f -> + cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n. + Proof. + induction 2 as [| A n H'0 H'1 x H'2]; auto with sets. + rewrite (image_empty f). + intros n' CE. + apply cardinal_unicity with V (Empty_set V); auto with sets. + intro n'. + rewrite (Im_add A x f). + intro H'3. + elim cardinal_Im_intro with A f n; trivial with sets. + intros i CI. + lapply (H'1 i); trivial with sets. + cut (~ In _ (Im A f) (f x)). + intros H0 H1. + apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets. + apply card_add; auto with sets. + rewrite <- H1; trivial with sets. + red in |- *; intro; apply H'2. + apply In_Image_elim with f; trivial with sets. + Qed. + + Lemma cardinal_decreases : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n. + Proof. + induction 1 as [| A n H'0 H'1 x H'2]; auto with sets. + rewrite (image_empty f); intros. + cut (n' = 0). + intro E; rewrite E; trivial with sets. + apply cardinal_unicity with V (Empty_set V); auto with sets. + intro n'. + rewrite (Im_add A x f). + elim cardinal_Im_intro with A f n; trivial with sets. + intros p C H'3. + apply le_trans with (S p). + apply card_Add_gen with V (Im A f) (f x); trivial with sets. + apply le_n_S; auto with sets. + Qed. + + Theorem Pigeonhole : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal U A n -> + forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f. + Proof. + unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I. + cut (n' = n). + intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n). + apply injective_preserves_cardinal with (A := A) (f := f) (n := n); + trivial with sets. + Qed. + + Lemma Pigeonhole_principle : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> + forall n':nat, + cardinal _ (Im A f) n' -> + n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y). + Proof. + intros; apply not_injective_elim. + apply Pigeonhole with A n n'; trivial with sets. + Qed. -Lemma Im_def : - forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x). -Proof. -intros X f x H'; try assumption. -apply Im_intro with (x := x); auto with sets. -Qed. -Hint Resolve Im_def. - -Lemma Im_add : - forall (X:Ensemble U) (x:U) (f:U -> V), - Im (Add _ X x) f = Add _ (Im X f) (f x). -Proof. -intros X x f. -apply Extensionality_Ensembles. -split; red in |- *; intros x0 H'. -elim H'; intros. -rewrite H0. -elim Add_inv with U X x x1; auto with sets. -destruct 1; auto with sets. -elim Add_inv with V (Im X f) (f x) x0; auto with sets. -destruct 1 as [x0 H y H0]. -rewrite H0; auto with sets. -destruct 1; auto with sets. -Qed. - -Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V. -Proof. -intro f; try assumption. -apply Extensionality_Ensembles. -split; auto with sets. -red in |- *. -intros x H'; elim H'. -intros x0 H'0; elim H'0; auto with sets. -Qed. -Hint Resolve image_empty. - -Lemma finite_image : - forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f). -Proof. -intros X f H'; elim H'. -rewrite (image_empty f); auto with sets. -intros A H'0 H'1 x H'2; clear H' X. -rewrite (Im_add A x f); auto with sets. -apply Add_preserves_Finite; auto with sets. -Qed. -Hint Resolve finite_image. - -Lemma Im_inv : - forall (X:Ensemble U) (f:U -> V) (y:V), - In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y. -Proof. -intros X f y H'; elim H'. -intros x H'0 y0 H'1; rewrite H'1. -exists x; auto with sets. -Qed. - -Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. - -Lemma not_injective_elim : - forall f:U -> V, - ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y). -Proof. -unfold injective in |- *; intros f H. -cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)). -2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); - trivial with sets. -destruct 1 as [x C]; exists x. -cut (exists y : _, ~ (f x = f y -> x = y)). -2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y); - trivial with sets. -destruct 1 as [y D]; exists y. -apply imply_to_and; trivial with sets. -Qed. - -Lemma cardinal_Im_intro : - forall (A:Ensemble U) (f:U -> V) (n:nat), - cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p. -Proof. -intros. -apply finite_cardinal; apply finite_image. -apply cardinal_finite with n; trivial with sets. -Qed. - -Lemma In_Image_elim : - forall (A:Ensemble U) (f:U -> V), - injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x. -Proof. -intros. -elim Im_inv with A f (f x); trivial with sets. -intros z C; elim C; intros InAz E. -elim (H z x E); trivial with sets. -Qed. - -Lemma injective_preserves_cardinal : - forall (A:Ensemble U) (f:U -> V) (n:nat), - injective f -> - cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n. -Proof. -induction 2 as [| A n H'0 H'1 x H'2]; auto with sets. -rewrite (image_empty f). -intros n' CE. -apply cardinal_unicity with V (Empty_set V); auto with sets. -intro n'. -rewrite (Im_add A x f). -intro H'3. -elim cardinal_Im_intro with A f n; trivial with sets. -intros i CI. -lapply (H'1 i); trivial with sets. -cut (~ In _ (Im A f) (f x)). -intros H0 H1. -apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets. -apply card_add; auto with sets. -rewrite <- H1; trivial with sets. -red in |- *; intro; apply H'2. -apply In_Image_elim with f; trivial with sets. -Qed. - -Lemma cardinal_decreases : - forall (A:Ensemble U) (f:U -> V) (n:nat), - cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n. -Proof. -induction 1 as [| A n H'0 H'1 x H'2]; auto with sets. -rewrite (image_empty f); intros. -cut (n' = 0). -intro E; rewrite E; trivial with sets. -apply cardinal_unicity with V (Empty_set V); auto with sets. -intro n'. -rewrite (Im_add A x f). -elim cardinal_Im_intro with A f n; trivial with sets. -intros p C H'3. -apply le_trans with (S p). -apply card_Add_gen with V (Im A f) (f x); trivial with sets. -apply le_n_S; auto with sets. -Qed. - -Theorem Pigeonhole : - forall (A:Ensemble U) (f:U -> V) (n:nat), - cardinal U A n -> - forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f. -Proof. -unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I. -cut (n' = n). -intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n). -apply injective_preserves_cardinal with (A := A) (f := f) (n := n); - trivial with sets. -Qed. - -Lemma Pigeonhole_principle : - forall (A:Ensemble U) (f:U -> V) (n:nat), - cardinal _ A n -> - forall n':nat, - cardinal _ (Im A f) n' -> - n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y). -Proof. -intros; apply not_injective_elim. -apply Pigeonhole with A n n'; trivial with sets. -Qed. End Image. + Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file |