diff options
Diffstat (limited to 'theories/Sets/Image.v')
| -rwxr-xr-x | theories/Sets/Image.v | 244 |
1 files changed, 125 insertions, 119 deletions
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index d5f42e3f9..85b83d3ab 100755 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -39,161 +39,167 @@ Require Export Le. Require Export Finite_sets_facts. Section Image. -Variables U, V: Type. +Variables U V : Type. -Inductive Im [X:(Ensemble U); f:U -> V]: (Ensemble V) := - Im_intro: (x: U) (In ? X x) -> (y: V) y == (f x) -> (In ? (Im X f) y). +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: - (X: (Ensemble U)) (f: U -> V) (x: U) (In ? X x) -> (In ? (Im X f) (f x)). +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. +intros X f x H'; try assumption. +apply Im_intro with (x := x); auto with sets. Qed. -Hints Resolve Im_def. +Hint Resolve Im_def. -Lemma Im_add: - (X: (Ensemble U)) (x: U) (f: U -> V) - (Im (Add ? X x) f) == (Add ? (Im X f) (f x)). +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; Intros x0 H'. -Elim H'; Intros. -Rewrite H0. -Elim Add_inv with U X x x1; Auto with sets. -NewDestruct 1; Auto with sets. -Elim Add_inv with V (Im X f) (f x) x0; Auto with sets. -NewDestruct 1 as [x0 H y H0]. -Rewrite H0; Auto with sets. -NewDestruct 1; Auto with sets. +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: (f: U -> V) (Im (Empty_set U) f) == (Empty_set V). +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. -Intros x H'; Elim H'. -Intros x0 H'0; Elim H'0; Auto with sets. +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. -Hints Resolve image_empty. +Hint Resolve image_empty. -Lemma finite_image: - (X: (Ensemble U)) (f: U -> V) (Finite ? X) -> (Finite ? (Im X f)). +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. +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. -Hints Resolve finite_image. +Hint Resolve finite_image. -Lemma Im_inv: - (X: (Ensemble U)) (f: U -> V) (y: V) (In ? (Im X f) y) -> - (exT ? [x: U] (In ? X x) /\ (f x) == y). +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. +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] (x, y: U) (f x) == (f y) -> x == y. +Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. -Lemma not_injective_elim: - (f: U -> V) ~ (injective f) -> - (EXT x | (EXT y | (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; Intros f H. -Cut (EXT x | ~ ((y: U) (f x) == (f y) -> x == y)). -2: Apply not_all_ex_not with P:=[x:U](y: U) (f x) == (f y) -> x == y; - Trivial with sets. -NewDestruct 1 as [x C]; Exists x. -Cut (EXT y | ~((f x)==(f y)->x==y)). -2: Apply not_all_ex_not with P:=[y:U](f x)==(f y)->x==y; Trivial with sets. -NewDestruct 1 as [y D]; Exists y. -Apply imply_to_and; Trivial with sets. +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: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) -> - (EX p: nat | (cardinal ? (Im A f) p)). +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. +intros. +apply finite_cardinal; apply finite_image. +apply cardinal_finite with n; trivial with sets. Qed. -Lemma In_Image_elim: - (A: (Ensemble U)) (f: U -> V) (injective f) -> - (x: U) (In ? (Im A f) (f x)) -> (In ? A x). +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. +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: - (A: (Ensemble U)) (f: U -> V) (n: nat) (injective f) -> (cardinal ? A n) -> - (n': nat) (cardinal ? (Im A f) n') -> n' = n. +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. -NewInduction 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; Intro; Apply H'2. -Apply In_Image_elim with f; Trivial with sets. +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: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) -> - (n': nat) (cardinal V (Im A f) n') -> (le n' n). +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. -NewInduction 1 as [|A n H'0 H'1 x H'2]; Auto with sets. -Rewrite (image_empty f); Intros. -Cut n' = O. -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. +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: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) -> - (n': nat) (cardinal V (Im A f) n') -> (lt n' n) -> ~ (injective f). +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; Intros A f n CAn n' CIfn' ltn'n I. -Cut n' = n. -Intro E; Generalize ltn'n; Rewrite E; Exact (lt_n_n n). -Apply injective_preserves_cardinal with A := A f := f n := n; Trivial with sets. +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: - (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) -> - (n': nat) (cardinal ? (Im A f) n') -> (lt n' n) -> - (EXT x | (EXT y | (f x) == (f y) /\ ~ x == y)). +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. +intros; apply not_injective_elim. +apply Pigeonhole with A n n'; trivial with sets. Qed. End Image. -Hints Resolve Im_def image_empty finite_image : sets v62. +Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file |