diff options
Diffstat (limited to 'theories/Relations/Relations.v')
| -rwxr-xr-x | theories/Relations/Relations.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index f792e4c2a..d2c3e2776 100755 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -12,17 +12,17 @@ Require Export Relation_Definitions. Require Export Relation_Operators. Require Export Operators_Properties. -Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B) - (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))). -Intros; Split; Elim H; Red; Auto. -Intros _ equiv_trans _ x y z H0 H1; Apply equiv_trans with (f y); Assumption. +Lemma inverse_image_of_equivalence : + forall (A B:Set) (f:A -> B) (r:relation B), + equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). +intros; split; elim H; red in |- *; auto. +intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. Qed. -Lemma inverse_image_of_eq : (A,B:Set)(f:A->B) - (equivalence A [x,y:A](f x)=(f y)). -Split; Red; -[ (* reflexivity *) Reflexivity -| (* transitivity *) Intros; Transitivity (f y); Assumption -| (* symmetry *) Intros; Symmetry; Assumption -]. -Qed. +Lemma inverse_image_of_eq : + forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y). +split; red in |- *; + [ (* reflexivity *) reflexivity + | (* transitivity *) intros; transitivity (f y); assumption + | (* symmetry *) intros; symmetry in |- *; assumption ]. +Qed.
\ No newline at end of file |