diff options
Diffstat (limited to 'theories/Sets/Infinite_sets.v')
-rw-r--r-- | theories/Sets/Infinite_sets.v | 388 |
1 files changed, 194 insertions, 194 deletions
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index 806e9dde..47554ac4 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Infinite_sets.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Infinite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Finite_sets. Require Export Constructive_sets. @@ -40,205 +40,205 @@ Require Export Finite_sets_facts. Require Export Image. Section Approx. -Variable U : Type. + Variable U : Type. -Inductive Approximant (A X:Ensemble U) : Prop := + 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. + 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. |