diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:12:20 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:12:20 +0000 |
commit | 639af2938c15202b12f709eb84790d0b5c627a9f (patch) | |
tree | 264517f1b305a703117e2b518a8088cbeed09524 /theories/Relations/Relations.v | |
parent | 71f380cb047a98d95b743edf98fe03bd041ea7bc (diff) |
theories/Relations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Relations/Relations.v')
-rwxr-xr-x | theories/Relations/Relations.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v new file mode 100755 index 000000000..f11537a6e --- /dev/null +++ b/theories/Relations/Relations.v @@ -0,0 +1,21 @@ + +(* $Id$ *) + +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; Apply equiv_trans with (f y); Assumption. +Save. + +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 +]. +Save. |