summaryrefslogtreecommitdiff
path: root/theories/Sets/Infinite_sets.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sets/Infinite_sets.v')
-rw-r--r--theories/Sets/Infinite_sets.v388
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:04:21 +0000